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
0answers
17 views

Hilbert Transform Calculation of a pulse

Can anybody help me with the Hilbert transform of the following pulse: $$ p(t) = \frac{8B\rho \cos(2\pi Bt+2\pi B\rho t)+\frac{\sin(2\pi Bt-2\pi B\rho t)}{t}}{\pi\sqrt{2B}(1-64(B\rho t)^2)} $$ I tried ...
1
vote
1answer
41 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
1answer
35 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))→...
2
votes
1answer
69 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
2answers
54 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)(((\...
1
vote
0answers
42 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
2answers
87 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 ...
1
vote
1answer
50 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 ...
2
votes
1answer
102 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 ...
2
votes
1answer
80 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
0answers
24 views

Show that $\operatorname{Im}(G)$ is the Hilbert Transform of $\operatorname{Re}(G)$

Given that $\operatorname{G}: \mathbb{R} \rightarrow \mathbb{C}$ is such that $\widehat{\operatorname{G}}(w) = 0$ for $w < 0$, show that $\operatorname{Im}(\operatorname{G})$ is the Hilbert ...
0
votes
1answer
73 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 ...
1
vote
0answers
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(...
0
votes
0answers
40 views

Is there a Hilbert-style Axiom system for Classical Propositional Logic where formulae are in negation normal form?

The wiki page (https://en.wikipedia.org/wiki/List_of_Hilbert_systems) has a list of various axiom systems for classical propositional logic (CPL), however, the page omits mention of an axiomatisation ...
3
votes
2answers
61 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
1answer
17 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 ...
2
votes
1answer
133 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 ...
1
vote
2answers
121 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 ...
0
votes
0answers
20 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
0answers
26 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
1answer
32 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,...
1
vote
1answer
91 views

Proof in Hilbert System [closed]

I'm new in proving propositional formulas, and have to prove the following formulas in the Hilbert system: $(¬Y→¬X)→(X→Y)$ $(X→Y)→(¬Y→¬X)$ The Hilbert system has $¬$ and $→$ as primitives and Modus ...
5
votes
2answers
116 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 \...
3
votes
1answer
97 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)) \...
0
votes
0answers
44 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
1answer
51 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/...
0
votes
2answers
51 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)...
2
votes
0answers
85 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: ...
1
vote
0answers
40 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 ...
4
votes
1answer
121 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
2answers
89 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 →...
2
votes
1answer
46 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 ...
3
votes
1answer
131 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\...
3
votes
2answers
88 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}$. ...
2
votes
0answers
59 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 ...
1
vote
2answers
86 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) \...
0
votes
1answer
113 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
2answers
74 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) (¬β →...
2
votes
1answer
148 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
0answers
66 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 $ ...
0
votes
1answer
37 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 (...
1
vote
3answers
136 views

can we a prove ⊢ (α → α) → (α → α)

The system L0 is defined as follows: Axioms: A1 (α → (β → α)) A2 2. (α → (β → γ) → ((α → β) → (α → γ)) A3 ((¬β → ¬α) → ((¬β → α) → β)) In one of my problem sheets, I am told that I am allowed to ...
2
votes
2answers
62 views

Does the deduction theorem hold in Q?

The proof of the deduction theorem (for a system including Hilbert Calculus) that I am familiar with uses modus ponens to prove the result one way, and mathematical induction the other way. Robinson'...
0
votes
1answer
59 views

Hilbert Calculus Derivation

Im tryng to prove that this is a theorem using Hilbert calculus $(∀x_1 (∀x_2 (p(x_1) ⇒ ((¬ p(x_2)) ⇒ (¬(p(x_1) ⇒ p(x_2)))))))$ The problem is getting this part $(p(x_1) ⇒ ((¬ p(x_2)) ⇒ (¬(p(x_1) ⇒ p(...
1
vote
2answers
91 views

Prove $ (∀x_1 (∃x_2 (p(x_1, x_2) ⇒ (∀x_2 p(x_1, x_2)))))$

Can u help show that this is a theorem? $ (∀x_1 (∃x_2 (p(x_1, x_2) ⇒ (∀x_2 p(x_1, x_2)))));$ I was trying to use the deduction theorem but i hit a wall. Can u help me out using derivatives and ...
1
vote
0answers
78 views

Hilbert proof are there errors in these derivations?

I came a cross two Hilbert proofs In S4(first proof): $p \rightarrow K p$ (necessitation) $\neg K p \rightarrow K \neg Kp $ (substitution, 1) In T(second proof): $q \rightarrow K q$ (necessitation)...
1
vote
2answers
87 views

Prove distribution of or over implies knowing the implication is always true

I was given a task to construct a Hilbert-style proof for the following: $A → B ⊢ C ∨ A → C ∨ B$ I figured I could use the axiom $A→B≡A∨B≡B$, but this leads me nowhere since I don't think I can use ...
2
votes
3answers
262 views

Show that $\Sigma \vdash\varphi$ if and only if $\Sigma\,\cup \{\neg\varphi\}$ is inconsistent.

I am stuck at the following problem: Let $\varphi$ be a sentence in a predicate calculus $T$ and $\Sigma$ a set of sentences in $T$. Show that $\Sigma \vdash\varphi$ if and only if $\Sigma\,\cup \{\...
7
votes
1answer
434 views

Relationship between sequent calculus and Hilbert systems, natural deduction, etc

I am trying to learn the basics of logic and I'm confused on how these proof systems work together. The big ones I see are Hilbert style, and then Gentzen style which includes natural deduction, and ...
2
votes
1answer
254 views

When does $(\square P \land \square Q) \to \square (P \land Q)$ hold?

If all axioms of classical propositional calculus hold and we work in modal logic that is at least K (ie. extremely weak), it is trivial to show $\square(P \land Q) \to (\square P \land \square Q)$. ...