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.

Filter by
Sorted by
Tagged with
0 votes
1 answer
119 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( \...
  • 109
3 votes
1 answer
324 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-...
  • 4,410
7 votes
6 answers
462 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 ...
  • 13.7k
3 votes
2 answers
129 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 ...
1 vote
2 answers
73 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 ...
0 votes
1 answer
110 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 ...
  • 121
1 vote
1 answer
98 views

Proving $\lnot((A\Rightarrow B)\Rightarrow\lnot(B\Rightarrow C))\Rightarrow(A\Rightarrow C)$

I want to find a proof for $\lnot \left( \left( A\Rightarrow B\right) \Rightarrow \lnot \left( B\Rightarrow C\right) \right) \Rightarrow \left( A\Rightarrow C\right)$ with these four axioms: (A1) $A\...
  • 11
1 vote
1 answer
134 views

How to prove this theorem in this hilbert system

I want to find a proof for $((\alpha \rightarrow (\beta \rightarrow \gamma))\rightarrow ((\alpha \rightarrow \beta)\rightarrow(\alpha \rightarrow \gamma)))$ with these three axioms: Ax1: $(\alpha \...
1 vote
1 answer
74 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$. ...
0 votes
2 answers
191 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'...
5 votes
2 answers
111 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 ...
1 vote
0 answers
72 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 ...
  • 1,882
1 vote
0 answers
51 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
1 answer
64 views

Choice of postulate 1b in Kleene's Introduction to Metamathematics

In Introduction to Metamathematics, Kleene introduces a formal system where the first three postulates in the group for propositional calculus are: $$ 1a. A \to (B \to A)\\ 1b. (A \to B) \to ((A \to (...
2 votes
1 answer
51 views

Prove that {A ⇒ ¬C, ¬A ⇒ B} ⊢ C ⇒ B using only Modus Ponens, the typical theorem (A → ¬C) → (C → ¬A) and 3 axioms.

I have an exercise where I have to prove the given sentence {A ⇒ ¬C, ¬A ⇒ B} ⊢ C ⇒ B using only Modus Ponens, the typical theorem (A → ¬C) → (C → ¬A) and the following three axioms: A→(B→A) (A→(B→C))→...
  • 69
2 votes
1 answer
245 views

Prove double negation introduction with this axiom system.

I want to find a proof for ( $⊢A \rightarrow ¬¬A $ ) with these four axioms: A1: $ A \rightarrow (B\rightarrow A) $ A2: $ (A \rightarrow (B\rightarrow C)) \rightarrow ((A\rightarrow B)\rightarrow(A\...
1 vote
2 answers
63 views

Axiomatic Schema Substitution

With the following axiomatic schema (A1 - A3) $(A1)(B \rightarrow (C \rightarrow B))$ $(A2)((B \rightarrow (C \rightarrow D)) \rightarrow ((B \rightarrow C) \rightarrow (B \rightarrow D)))$ $(A3)(((\...
user avatar
1 vote
0 answers
55 views

Are my instantiations of Axiom 5 (Mendelson) correct?

I'm reading "Introduction to mathematical logic" from Mendelson. I'm in chapter 2 "First-order logic and Model theory".I am interested in learning the axiomatic method without ...
0 votes
2 answers
135 views

Should $\vdash$ in Theorem 24B In Enderton's logic book be $\models$ instead?

SECTION 2.4 A Deductive Calculus In Enderton's A Mathematical Introduction to Logic divides the set of axioms into several groups. The first group is called "tautologies" on p114, which are ...
  • 45k
1 vote
1 answer
122 views

How are tautology axioms in a Hilbert system for FOL obtained from tautologies in Sentential Logic?

SECTION 2.4 A Deductive Calculus In Enderton's A Mathematical Introduction to Logic divides the set of axioms into several groups. The first group is called "tautologies" on p114, which are ...
  • 45k
2 votes
1 answer
241 views

Do inference rules mean the same in a Hilbert system and in a natural deductive system?

Is it correct that Enderton's A Mathematical Introduction to Logic uses a Hilbert style system for first order logic? On p110 in SECTION 2.4 A Deductive Calculus in Chapter 2: First-Order Logic Our ...
  • 45k
2 votes
1 answer
140 views

Is my derivation of $\vdash (\forall x)(B \implies C) \implies ((\forall x)B \implies (\forall x)C)$ correct?

I'm reading Introduction to mathematical logic from Mendelson. I'm in chapter 2 "First-order logic and Model theory". Axioms are: ($A1$): $B ⇒ (C ⇒ B)$ ($A2$): $(B ⇒ (C ⇒ D)) ⇒ ((B ⇒ C) ⇒ (B ...
0 votes
1 answer
302 views

Proving ⊢ A∨(A→B) using Hilbert system

I'm self-studying mathematical logic from "Introduction to Mathematical Logic" by Detlovs and Podnieks (available free here under CC license). Unfortunately, it doesn't come with any ...
user avatar
1 vote
0 answers
18 views

Proof verification: $\vdash ((\forall x_1 (\forall x_2 p(x_1, x_2))) \implies p(f(x_1, x_2), x_2))$.

I need to check if my proof for $\vdash_\Sigma ((\forall x_1 (\forall x_2 p(x_1, x_2))) \implies p(f(x_1, x_2), x_2))$ is correct for $x_1,x_2 \in X$, $f(x_1,x_2) \in T_\Sigma$ and $p \in P_2$. Def(...
3 votes
2 answers
112 views

Transforming Hilbert-style Axiom Systems for Classical Propositional Logic and Retaining Soundness and Completeness

First off, I will use ~ for negation, & for conjunction, V for disjunction, -> for implication, and <-> for bi-conditional. To the question: The axioms of classical propositional logic (CPL) ...
0 votes
1 answer
29 views

Proving a linear form to be continuous

In the Hilbert space $L^2(R)$ I have seen that the following form is linear, however, I need to check if it is continuous and find the associated vector using the Riesz-Fréche Theorem. I have tried to ...
  • 63
2 votes
1 answer
494 views

Proving $\vdash \neg \neg P \to P$ in first order logic, preferrably without deduction theorem

The axiom system used is $A\to B \to A$ $(A \to B \to C) \to (A \to B) \to A \to C$ $(\neg A \to \neg B)\to (B \to A)$ $(\forall x A) \to A[t/x]$, where $x$ is substitutable with $t$ in $A$. $\forall ...
  • 3,339
1 vote
2 answers
371 views

Prove the introduction of conjunction using axioms in a Hilbert system

Given a Hilbert system with the axioms (and of course the Modus Ponens): $ A1.\ \phi \to \phi \\ A2.\ \phi \to ( \psi \to \phi ) \\ A3.\ ( \phi \to ( \psi \to \xi )) \to (( \phi \to \psi ) \to ( \phi ...
  • 141
0 votes
0 answers
25 views

Syntactical proof in a Hilbert system without additional lemmas [duplicate]

How do I proof $\neg \neg p \rightarrow p$ in the following Hilbert system without the use of additional lemmas (derive purely syntactical)? $A \rightarrow (B \rightarrow C)$ $(A \rightarrow (B \...
1 vote
0 answers
27 views

Translation rules in Hilbert Calculus

I am trying to prove the fact $A \supset B, A \supset C \vdash A \supset (B \land C)$ in a hilbert-type system. However, I am struggling to find a translation rule for $B \land C$. Citing from my ...
0 votes
1 answer
34 views

Multiple solutions for {↓} ⊢ (p → r) → r

Are both of these correct? Teacher's solution {↓} ⊢ (p → r) → r {↓ , (p → r)} ⊢ r 1 ((p → ↓) → ↓) → p Ax3 F/p 2 ↓ → ((p → ↓) → ↓) Ax2 F/↓ G/(p → ↓) 3 ↓ ∈ Σ 4 ((p → ↓) → ↓) MP 2,...
5 votes
2 answers
144 views

Hilbert System Logical Axiom 1 follows from Axioms 2 and 3

I'm reading Wikipedia and it lists the first four logical axioms that allow (together with modus ponens) for the manipulation of logical connectives. $\phi \to \phi $ $\phi \to \left(\psi \to \phi \...
  • 172
3 votes
1 answer
275 views

What is the proof of reductio ad absurdum (RAA) in a Łukasiewicz axiom system for propositional logic with only modus ponens?

I am working with the following Lukasiewicz axiom system: Axiom Schema 1: $\alpha \rightarrow (\beta \rightarrow \alpha )$ Axiom Schema 2: $(\alpha \rightarrow (\beta \rightarrow \gamma)) \...
  • 685
0 votes
0 answers
62 views

Show that a Rule is Derivable in a Hilbert Calculus

Is my answer to the following question correct? Discuss whether a rule of "partial generalization", i.e. $\frac{H(x)\rightarrow Gx}{\forall x H(x) \rightarrow \exists x Gx}$ is derivable as an ...
0 votes
1 answer
69 views

Prove that $\alpha\vdash\beta$ implies $\alpha\vee\gamma\vdash\beta\vee\gamma$ using four unary Hilbert-style rules of inference.

We have a calculus $\vdash$ in the set $\mathcal{F}\{\vee\}$ of propositional formulas with the signature $\{\vee\}$. It has the following four unary Hilbert-style rules: $$ \begin{align} (1)\ \alpha/...
  • 33
0 votes
2 answers
90 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)...
  • 73
2 votes
0 answers
291 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
0 answers
78 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
4 votes
1 answer
315 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
2 answers
134 views

Deductive proof with Hilbert system

Given b→a, and⌝(a→⌝b) I'm trying to derive b. Obviously I can use some identities (like De Morgan) to show that ⌝(a→⌝b) is equivalent a∧b. However, I'd like to avoid using any other connectives than →...
  • 85
2 votes
1 answer
65 views

What are the restrictions on substitution of terms in Hilbert-style calculus vis-à-vis intuitionistic logic?

I apologize if the title of this question can be better formulated, but I recently encountered a situation where what I thought was valid substitution led to an incorrect thing—at least I think. I ...
2 votes
1 answer
302 views

Propositional Logic - How to prove that A implies itself? [duplicate]

I'm trying to form a propositional logic proof chain for the tautology $\delta \implies \delta$, using only the axioms $\alpha \implies (\beta \implies \alpha)$ $((\alpha\implies (\beta \implies\...
4 votes
2 answers
119 views

What is the probability of randomly generating a tautology?

Suppose we randomly generate a classical Hilbert propositional calculus formula $F$ with $n$ variables, using the following method: $F = x_i$ for each of $i \leq n$ with probability $\frac{1}{n+2}$. ...
  • 15.1k
3 votes
0 answers
90 views

Hilbert calculi for First-Order Logic

I'm a bit confused about the Hilbert-style axiomatization of first-order logic. More precisely, I am a bit confused about completeness w.r.t. to Hilbert-calculi. A complete Hilbert-style calculus I am ...
  • 4,632
1 vote
2 answers
125 views

using modus ponens to deduce $(\neg A \rightarrow \neg B) \rightarrow ((\neg A \rightarrow B) \rightarrow A)$

Given The following 3 axioms: $B \rightarrow (A \rightarrow B)$ $(B \rightarrow (A \rightarrow C)) \rightarrow ((B \rightarrow A) \rightarrow (B \rightarrow C))$ $(\neg A \rightarrow \neg B) \...
  • 67
0 votes
1 answer
269 views

Proving that a set of formulas are closed under logical consequence

My textbook defines a theory as a set of formulas that is closed under logical consequence. According to the book, a set of formulas U is closed under logical consequence iff for all formulas A, if $$...
0 votes
2 answers
121 views

How to prove ⊢ (B → ¬B) → ¬B using an informal deduction

So I need to prove ⊢ (B → ¬B) → ¬B I can use the Modus ponus (MP) rule, and deduction theorem (DT). And I have these 3 axioms: α → (β → α) --- (A1) (α → (β → γ)) → ((α → β) → (α → γ)) --- (A2) (¬β →...
  • 23
2 votes
1 answer
420 views

Axiomatic proofs in propositional logic

I have to use these three axioms (A1) $P \to (Q \to P)$ (A2) $(P \to (Q \to R)) \to ((P \to Q) \to (P \to R))$ (A3) $(\neg Q \to \neg P) \to ((\neg Q \to P) \to Q)$ along with Modus Ponens to ...
1 vote
0 answers
70 views

What is the characteristic equation of this linear ODE?

I am trying to solve the following linear ODE for $y(x)$: $$y^{\prime\prime\prime}+y^{\prime\prime}+\mathcal{H}[y^{\prime\prime}]+y^\prime-cy=0$$ subject to the boundary conditions $y\rightarrow0 $ ...
  • 481
0 votes
1 answer
75 views

Classical Propositional Logic and Axioms

We define a new proof system N over the connectors: {∨,¬} For every α and β- 𝐴1: (𝛼 ∨ (𝛽 ∨ (¬𝛼))) (axiom) Deductions: 𝑀𝑃1: if we have 𝛼, 𝛽 then we can deduce (¬(¬(α∨β))) 𝑀𝑃2: if we have (...
  • 89