# 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
Filter by
Sorted by
Tagged with
73 views

156 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))$ (Hypothesis)...
23 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
83 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 ...
82 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 ...
21 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!
62 views

• 101
661 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,501
774 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.3k
157 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
97 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
167 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
1 vote
108 views

1 vote
146 views

### Is the following definition of orthonormal basis in Hilbert space?

Let $H$ Hilbert, then $\{e_n \} \subset H$ is an orthonormal basis of $H$ if $|e_n|=1$ for every $n$, $\langle e_n,e_m \rangle =0$ for every $m,n$ and $\overline {\operatorname{span}(\{e_n \})}=H$. ...
• 123
308 views

### Constructing Hilbert-style proofs without "assume" structure

According to the definition of Hilbert-style systems, proofs should be constructed only by applying axioms and rules of inference. In practice, most proof that I have seen use the 'suppose' or 'assume'...
• 215
156 views

### strong completeness of a formal system

Given a formal system $D$ where the axioms are the same as in Hilbert system for propositional logic and the inference rule is $$\frac{a\rightarrow b, \quad a\rightarrow \neg b}{\neg a}$$ I need to ...
• 393
1 vote
98 views

### Do we have to use free variables in Hilbert systems?

I find it very unpleasant using free variables in proofs, because it puts lines in proofs which have no intuitive meaning. This is clearly necessary for natural deduction, but I was wondering if it ...
• 2,326
1 vote
55 views

### Reference for proof of completeness of classical predicate logic in a Hilbert system

Many proofs of the completeness of classical logic with respect to some particular Hilbert style atomization of it do not explicitly reference the axioms at hand. The devils must be buried in the ...
• 369
1 vote
79 views

• 43
101 views

### changing the axiom $\forall x(A(x) \to B) \to (\exists xA(x)\to B)$ of Hilbert proof system for perdicate logic

What type of logic would it be if we change the axiom $$\text{old} = \forall x(A(x) \to B) \to (\exists xA(x)\to B)$$ to the new rule  \text{new} = \forall x(A(x) \to B) \to (\forall xA(x)\to B)...
• 91
561 views

### How to prove that ├ (¬¬φ⇒φ) and ├ (φ⇒¬¬φ) based on deduction and/or proof by contradiction? [duplicate]

EDIT: someone just showed my the typo in the lecture notes. instead of: {¬¬φ,φ}├ φ {¬¬φ,φ}├ ¬φ it should be: ...
• 91
1 vote
94 views

### help to prove the logical expression ¬¬A→A in HPC proof system [duplicate]

I'm trying to prove the expression ¬¬A→A. I can use 3 axioms: A1: a→(b→a) A2: (a→(b→c))→((a→b)→(a→c)) A3: (¬b→¬a)→(a→b), MP rule and deduction theorem. What am I doing wrong? ⊢ ¬¬A → A ¬¬A ⊢A ...
• 11
400 views

### How to prove $((A \to B) \to A) \to A$ using Lukasiewicz's axioms, MP and deduction theorem?

This is an exercise from A.G. Hamilton's Logic for Mathematicians, section 2.1, p. 36. I have tried to do this for 10 long years, since 2010. Unsuccessful. Exercise 3: Using the deduction theorem ...
1 vote