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.
102
questions
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 ...
- 175
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 ...
- 13
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 \...
- 293
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$.
...
- 95
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'...
- 215
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 ...
- 383
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 (...
- 133
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\...
- 293
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)(((\...
user713989
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 ...
- 246
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 ...
- 246
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 ...
user383527
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) ...
- 31
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 \...
- 11
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,...
- 103
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 ...
- 217
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 ...
- 809
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 ...
- 123
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 ...
- 29
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