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
73 views

Help with proofs in Hilbert Style system

We have a set of derivability-statements of the following form: $\vdash A \rightarrow A \qquad$ Trivial Implication $\vdash \neg\neg A \rightarrow A \qquad$ Remove double Negation $\...
DDD's user avatar
  • 11
0 votes
1 answer
98 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, ...
The Sea's user avatar
0 votes
1 answer
71 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 (...
Jeroen van Rensen's user avatar
0 votes
0 answers
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)...
Blue Jay's user avatar
0 votes
0 answers
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 ...
lightyourassonfire's user avatar
1 vote
1 answer
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 ...
Alexander Sanchez's user avatar
0 votes
2 answers
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 ...
Jonathan King's user avatar
0 votes
0 answers
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!
Jonathan King's user avatar
0 votes
0 answers
62 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 ...
jjbinks's user avatar
  • 71
0 votes
1 answer
203 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( \...
Arianna's user avatar
  • 101
3 votes
1 answer
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-...
Vivaan Daga's user avatar
  • 5,501
9 votes
6 answers
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 ...
kjo's user avatar
  • 14.3k
4 votes
2 answers
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 ...
KeizerHarm's user avatar
1 vote
2 answers
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 ...
ne.ko_92's user avatar
0 votes
1 answer
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 ...
Dedekind's user avatar
  • 183
1 vote
1 answer
108 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\...
Knn's user avatar
  • 11
1 vote
1 answer
193 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 \...
Omid Yaghoubi's user avatar
1 vote
1 answer
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$. ...
carlos85's user avatar
  • 123
0 votes
2 answers
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'...
Jencel's user avatar
  • 215
5 votes
2 answers
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 ...
CforLinux 's user avatar
1 vote
0 answers
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 ...
Thomas Anton's user avatar
  • 2,326
1 vote
0 answers
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 ...
Eoin's user avatar
  • 369
1 vote
1 answer
79 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 (...
Mircea Baja's user avatar
2 votes
1 answer
58 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))→...
ADbeat's user avatar
  • 69
2 votes
1 answer
350 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\...
Omid Yaghoubi's user avatar
1 vote
2 answers
69 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
65 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 ...
Mauro curto's user avatar
0 votes
2 answers
189 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 ...
Tim's user avatar
  • 47.2k
1 vote
1 answer
164 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 ...
Tim's user avatar
  • 47.2k
2 votes
1 answer
310 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 ...
Tim's user avatar
  • 47.2k
2 votes
1 answer
189 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 ...
Mauro curto's user avatar
1 vote
2 answers
589 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
22 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(...
Tomás Pacheco 's user avatar
3 votes
2 answers
163 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) ...
JoeSmith123's user avatar
0 votes
1 answer
50 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 ...
Ramon's user avatar
  • 63
2 votes
1 answer
795 views

Proving $\vdash \neg \neg P \to P$ (double negation elimination) 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 ...
Trebor's user avatar
  • 4,555
2 votes
2 answers
553 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 ...
Isti115's user avatar
  • 151
0 votes
0 answers
29 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 \...
John Eren's user avatar
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 ...
Rafael Bankosegger's user avatar
0 votes
1 answer
36 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,...
user4676310's user avatar
5 votes
2 answers
189 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 \...
jet457's user avatar
  • 524
3 votes
1 answer
417 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)) \...
Nika's user avatar
  • 727
0 votes
0 answers
77 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 ...
Moritz Loritz's user avatar
1 vote
2 answers
89 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/...
Keno's user avatar
  • 43
0 votes
2 answers
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)...
mike's user avatar
  • 91
2 votes
0 answers
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: ...
Zack's user avatar
  • 91
1 vote
0 answers
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 ...
Evster's user avatar
  • 11
4 votes
1 answer
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 ...
João Alves Jr.'s user avatar
1 vote
2 answers
171 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 →...
Ben's user avatar
  • 85
2 votes
1 answer
74 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 ...
philomathic_life's user avatar