Questions tagged [hilbert-calculus]
In logic a Hilbert calculus, sometimes called Hilbert system, Hilbert-style deductive system or Hilbert–Ackermann system, is a type of system of formal deduction attributed to Gottlob Frege and David Hilbert. These deductive systems are most often studied for propositional and first-order logic.
113
questions
0
votes
1
answer
71
views
What exactly is the propositional calculus that ZFC is founded on?
It's my understanding that ZFC is axiomatized in terms of propositional logic. However, propositional logic is just a logic which deals with propositions, and on its own has no inherent axioms. Yet, ...
- 275
0
votes
1
answer
103
views
Is $(\phi\implies\psi) \iff ((\phi\land\psi)\lor \neg\phi) $ provable in the following hilbert calculus without contraposition or reductio?
Is $(\phi\implies \psi) \iff ((\phi\land \psi)\lor \neg \phi) $ in the following hilbert calculus without contraposition or reductio ad absurdum? If so, how would I go about proving it, and if not, ...
- 1
1
vote
1
answer
90
views
Propositional logic without rules of inference and assumptions (except MP)
I was wondering whether it would be possible to do propositional logic without any rules of inference and assumptions (except modus ponens).
I have the following axioms:
$ p \to (q \to p) $
$ (p \to (...
0
votes
0
answers
172
views
Writing a Hilbert-style Proof for $(A ∧ (¬B)) ⊢ (¬(A → B)$
I've been trying to write a Hilbert-style proof using the Axioms and Rules of Inference for propositional logic, but I keep getting stuck at step 3.
$$(A ∧(¬B)) ⊢ (¬(A → B)$$
$(A ∧ (¬B))$ (...
- 1
1
vote
1
answer
36
views
What is $r^{-1}(B)$ if $r$ is a rule and $B$ is an expression in a proof system?
In the first paragraph, what does $r^{-1}(B)$ mean? Does it have something to do with relations? e.g if $A$ is a relation then $A^{-1}$ is the inverse of that relation.
Its from a paper about the ...
1
vote
1
answer
92
views
Theorems (or references to analysis) of a particular Hilbert-deductive-system using $\\{\neg, \wedge, \vee, \rightarrow\\}$ as primitive symbols?
Context
The System CL
In section 6.3 of Topoi, Robert Goldblatt describes a Hilbert-style deductive calculus (the only inference law is modus ponens) for the ...
0
votes
2
answers
124
views
Need help with Hilbert-style proof (Given ¬q and (¬p⇒(¬q⇒¬r)), prove (r⇒p))
Given $\neg q$ and $(\neg p⇒(¬q⇒¬r))$, prove $(r⇒p)$. I unfortunately can't figure out how to begin this proof. Do any of you have any idea how to begin this proof? I'd appreciate any help anyone can ...
0
votes
0
answers
22
views
Need help with Hilbert-style proof.
Given ¬q and (¬p⇒(¬q⇒¬r)), prove (r⇒p).
Do any of you know how to do this? I appreciate whatever help you can provide me.
Thank you!
0
votes
0
answers
64
views
Proof in Natural Deduction, Sequent Calculus or Hilbert System
Is there any smart way to check if certain statements are not provable in any of these proof systems?
Like for example the following task:
Prove or disprove the following statements:
$\vDash \exists ...
- 71
0
votes
1
answer
220
views
Hilbert style proof of $\text{A}\vdash \left( \text{A}\to \text{B} \right)\to \text{B}$
Could somebody give a hint how to prove the following theorem $\text{A}\vdash \left( \text{A}\to \text{B} \right)\to \text{B}$ using a Hilbert style proof?
Three axiom schemas
(A1) $\alpha \to \left( \...
- 101
3
votes
1
answer
715
views
Is this Hilbert proof system complete?
Note: This post considers propositional logic, with $\to$, $\bot$ as the base connectives, $\neg \phi$ is an abbreviation for $\phi\to \bot$.Consider a usual Hilbert-style proof system(with modus-...
- 5,724
9
votes
6
answers
882
views
What is the motivation for the axioms for Propositional Calculus in Mendelson's "Introduction to Mathematical Logic"?
On pp. 26-27 of his Introduction to Mathematical Logic (5th edition), Elliott Mendelson writes:
If $\mathscr{B}$, $\mathscr{C}$, and $\mathscr{D}$ are wfs of $\mathrm{L}$, then the following are ...
- 14.5k
4
votes
2
answers
173
views
Axiomatic derivation - what does instancing an axiom practically entail?
I'm stunned by the chapter in my coursebook (which is in Dutch, so please advice if I am mistranslating any of the terms) about deriving from a system of axioms and derivation rules. The exercise is ...
- 185
1
vote
2
answers
99
views
Bound variables and two variables in a proposition
I'm trying to derive the following as a theorem in a FOL Hilbert system:
$$∀x∃yQ(xy) → ∃yQ(yy) $$
But I'm a bit confused as to how one should interpret the incidence of two variables in $Q$. Is there ...
- 13
0
votes
1
answer
223
views
Formal proof that $\vdash (\varphi \rightarrow \psi) \rightarrow (\neg \varphi \lor \psi)$.
I have to prove the statement
$$\vdash (\varphi \rightarrow \psi) \rightarrow (\neg \varphi \lor \psi)$$
only using first order logical axioms (similar to the ones in the Hilbert System), modus ponens ...
- 183