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.
93
questions
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)$. ...
