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.
1
vote
1answer
37 views
Help with Hilbert Calculus
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
31 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
49 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
82 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 \{\...
2
votes
1answer
101 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
140 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)$. ...
5
votes
2answers
122 views
Derive $P \to \neg \neg P$ in a structure with not and implies
We can define an abstract system with the following three axiom schemes that define $\to$ and $\lnot$ as follows:
ax1. $P\to(Q\to P)$
ax2. $(\lnot Q \to \lnot P)\to(P\to Q)$
ax3. $(P\to(Q\to R))\to(...
0
votes
0answers
16 views
Hilbert-style axioms for Boolean algebra
Is there some way to define boolean algebra without using any equalities. Kind of like the Hilbert system for propositional logic. Basically: let's restrict our algebra to just $\lnot$ and $\lor$. ...
0
votes
0answers
14 views
Proving $\vdash p\implies(\neg p \implies q)$ in Hilbert's system. [duplicate]
I've been given the following statement to prove using the three axioms in Hilbert's system and Modus Ponens: $\vdash p\implies(\neg p \implies q)$. This statement is taken from Derek Goldrei's ...
0
votes
0answers
70 views
What does semantic entailment even mean, in the context of completeness?
I tried to prove the soundness of a Hilbert system over in this post and so now I am trying to prove completeness from the other direction:
$$\Gamma \models \varphi \implies \Gamma \vdash \varphi$$
...
2
votes
1answer
70 views
Proving soundness property of a Hilbert system
Now that I have a better understanding of soundness, I'd like to try this again.
My goal is to prove that the classical Hilbert system has the soundness property:
$$\Gamma \vdash \varphi \implies \...
2
votes
1answer
150 views
How can we prove soundness property if it's possible for our assumption set to contain false assumptions? [duplicate]
Soundness property, to my knowledge is the property that:
$\Gamma \vdash \varphi \implies \Gamma \vDash \varphi$
If $\varphi$ is provable (a syntactic consequence) from $\Gamma$ then $\varphi$ is ...
1
vote
1answer
55 views
If $A \vdash a$ and $B \vdash b$ then $A \cup B \vdash a$ and $A \cup B \vdash b$? Question about the empty set and axioms.
Is it true/accepted that:
If $A \vdash a$ and $B \vdash b$ then $A \cup B \vdash a$ and $A \cup B \vdash b$?
Is there a name for this concept? Does it require its own meta-proof or is it just a ...
2
votes
1answer
69 views
Questions about proving $\lnot \lnot a = a$
This is all in the context of a Hilbert system with modus ponens $A, A\to B \vdash B$ and axioms:
Axiom $1$: $A \to (B \to A)$
Axiom $2$: $(A \to (B \to C)) \to ((A \to B) \to (A \to C))$
Axiom $...
2
votes
1answer
68 views
Hilbert systems and natural deduction systems in terms of “context”
I was reading the Wiki article on Hilbert systems and came across this passage:
A characteristic feature of the many variants of Hilbert systems is
that the context is not changed in any of their ...
1
vote
0answers
51 views
Prove $\Sigma \vdash \lnot(\phi \rightarrow \psi)$ iff $\Sigma \vdash \phi$ and $\Sigma \vdash \lnot \psi.$
$\Sigma$ is a set of sentences, the set $ L$ consists of all axioms of the forms:
A1)
$ \ \phi \rightarrow (\psi \rightarrow \phi)$
A2) $\ (\phi \rightarrow (\psi \rightarrow \theta)) \rightarrow (...
-1
votes
1answer
72 views
Find a proof for the following tautology
I was introduced to Axiomatic Theory in last class and I need to know how to solve this kind of problem in the midterm next week. However, I have no idea how to solve these kind of problems. We had ...
0
votes
1answer
62 views
Formal Proof of WFF using Rules of Inference
I am currently hung up on a practice problem that requires a formal proof of a WFF using ONLY rules of inference. I've been attempting this for hours, but it seems like there is something i'm missing. ...
1
vote
1answer
85 views
How to prove $\lnot (\alpha \rightarrow \lnot \beta) \vdash \lnot (\beta \rightarrow \lnot \alpha)$ in HPC
I have the three axioms
$$\alpha \rightarrow (\beta \rightarrow \alpha)$$
$$\Big(\alpha \rightarrow (\beta \rightarrow\gamma)\Big)\rightarrow \Big((\alpha \rightarrow\beta)\rightarrow(\alpha\...
2
votes
1answer
121 views
A Hilbert-style proof that $\Gamma \vdash A \Rightarrow \Gamma \vdash B \Longleftrightarrow \Gamma \vdash A \to B$
The Hilbert-style system I am using consists of the following axioms:
$\phi \to (\psi \to \phi)$
$\phi \to (\psi \to \xi) \to ((\phi \to \psi) \to (\phi \to \xi))$
$(\neg\phi \to \psi) \to (\...
2
votes
2answers
68 views
Hilbert Calculus statement proof
I want to prove in $HPC$ that
$$ \vdash_{HPC} (A\rightarrow B)\rightarrow ((B\rightarrow C) \rightarrow (A\rightarrow C ))$$
I tried using different combinations of the $A\rightarrow (B \rightarrow ...
0
votes
2answers
64 views
Proof of $p\rightarrow(q\rightarrow r)\vdash_{HR} (p\rightarrow q)\rightarrow r$
Let HR be an Hilbert style proof system:
Inference rule: MP
Axiom schemes:
$A\rightarrow A$
$(A\rightarrow B)\rightarrow ((B\rightarrow C)\rightarrow(A\rightarrow C))$
$(A\rightarrow(B\rightarrow ...
0
votes
0answers
18 views
Did I understand well the Hilbert Transform?
Intro:
Find the Hilbert Transform of $x(t) = \mathrm{sinc}(t)\sin(\pi t)$
What I know:
I know the Hilbert Transform of signal $x(t)$ goes as $hx(t) = x(t) * \frac{1}{\pi t}$
(Where $hx$ stands for ...
0
votes
1answer
62 views
theoretical question regarding deduction and relation between $\vdash$ and $\vDash$
i have a very basic and theoritical question to help me understand the basics of logics and deduction systems. trying to understand the basics between the difference and deduction of $ \vdash$ $\vDash$...
1
vote
1answer
52 views
Hilbert style axiom system without generalisation
I the book Computational Complexity by C. Papadimitriou he introduces for first order logic the following axioms:
AX0: Any expression whose Boolean form is a tautology.
AX1: Any expression of ...
0
votes
3answers
62 views
Prove this $\vdash_{_L}\mathscr{\left((\neg B)\rightarrow B\right)\rightarrow B}$
The axioms of L are:
$\mathrm {(A1)} \quad \mathscr{\left(B\to\left(C\to B\right)\right)} \\ \mathrm {(A2)} \quad \mathscr{\left(\left(B\to\left(C\to D\right)\right)\to \left(\left(B \to C \right)\to ...
1
vote
1answer
81 views
Proving $\vdash_{HPI}A\vee(B\vee C) \rightarrow (A\vee B)\vee C $
Prove $\vdash_{HPI}A\vee(B\vee C) \rightarrow (A\vee B)\vee C $
From the axioms :
A1) A→(B→A)
A2) (A→(B→C))→((A→B)→(A→C))
A3) $(A\rightarrow B)\rightarrow((A\rightarrow\neg B)\rightarrow \neg A)$
...
0
votes
1answer
45 views
The most simple argument in an axiomatic system
I need to find the most simple argument to show that $\vdash_\mathcal{N}((a\rightarrow ((b\rightarrow c)\rightarrow (\lnot d\rightarrow c)))\rightarrow a)\rightarrow a$, where $\mathcal{N}$ has the ...
2
votes
2answers
184 views
Proofs using theorems instead of axioms [closed]
I'm not sure how to prove these basic theorems in propositional calculus. Instead of using the standard axioms, we're supposed to use:
Deduction Theorem (if $\Phi, \alpha \vdash \beta$ then $\Phi \...
1
vote
1answer
62 views
How to find a proof of a formula in propositional calculus?
$1.$ $\alpha$ $\rightarrow$$(\beta \rightarrow \alpha)$ --- (Ak)
$2.$ $(\alpha \rightarrow (\beta \rightarrow \gamma)) \rightarrow ((\alpha \rightarrow \beta ) \rightarrow (\alpha \...
0
votes
1answer
111 views
Hilbert's style sysytem without deductive theorem.
How to prove ¬P∨¬Q → ¬(P∧Q)
using the following axioms?
a1. A→(B→A)
a2. (A→(B→C))→((A→B)→(A→C))
a3.(A∧B)→A
a3'.(A∧B)→B
a4.A→(B→(A∧B))
a5. A→A∨B
a5'. B→A∨B
a6.(A→C)→((B→C)→(A∨B→C))
a7. ¬¬A→A
...
1
vote
0answers
69 views
Ridge Regression in Hilbert Space (RKHS)
I am looking for a nice, clean and proper derivation of the following statement:
Given:
$\arg\min_{f \in\mathcal{H}_K}\{||f-f_{p}||_p^2 +\lambda||f||^2_K\}$
where
$f_{p}(x) = \int_Y ydp(y|x)$,
$...
1
vote
1answer
91 views
Prove distributive law in Hilbert system
Using the logical axioms of the Hilbert system
$\phi\to\phi$
$\phi\to(\psi\to\phi)$
$\left( \phi \to \left( \psi \rightarrow \xi \right) \right) \to \left( \left( \phi \to \psi \right) \to \left( \...
2
votes
0answers
43 views
Sufficient condition for gradient existence in Hilbert spaces
Let $\mathbb H$ a Hilbert space and $N:\mathbb H\to \mathbb H$ a continuous nonlinear mapping. In Fonda and Mawhin (Iterative and variational methods for the solvability of some semilinear equations ...
1
vote
1answer
56 views
How does one create axiom schemata that will be able to generate all tautologies in the system?
To be more specific, how do I know that the axiom schemata(together with modus ponens) in the Hilbert calculus is able to generate all valid formulas in propositional calculus?
1
vote
1answer
344 views
Can we prove if ⊢ (α → β) and ⊢ (¬α → β) then ⊢ β in L0?
The system L0 is defined as follows:
Axioms:
A1 (α → (β → α))
A2 ((α → (β → γ)) → ((α → β) → (α → γ)))
A3 ((¬β → ¬α) → (α → β))
The only rule of inference is Modus Ponens:
MP From α and (α → β) ...
1
vote
1answer
32 views
Proving without the completeness theorem that variables can be renamed in Hilbert Calculus
Prove without the completeness theorem that for every formula $A$ and variables $x,y,z$, it holds that
$$\lnot\forall x\lnot A\left\{ x/z\right\} \vdash_{HC}\lnot\forall y\lnot A\left\{ y/z\right\} ...
1
vote
1answer
19 views
bilenear form extrema equality
Let $A$ a self-adjoint positive contnious operator from $H$ into $H$.
Do we have: $$sup(Ax,x) = \sup (Ax,y)$$ for all $||x|| = 1,||y|| = 1$?.
Thanks.
0
votes
2answers
142 views
Proving an extended of Hilbert System is not complete
Consider the following system, $S$ above $\{\lnot, \to, \lor \}$:
Axioms (1-3 are HPC's original ones):
$a\to (b\to a)$
$(a\to (b\to c))\to ((a\to b)\to (a\to c))$
$(\lnot a\to \lnot b)\to (b\to a)...
1
vote
1answer
82 views
Proof a rule to be admissible.
If I have a rule of the form $\phi_{0\dots n}/\psi$, can I show that it is admissible, i.e. that if all premises are true then the conclusion is also true by showing that $\models\bigwedge_{k=0}^{n}\...
1
vote
1answer
247 views
Proof soundness of a Hilbert Style Calculus
This is more a question about checking if my understanding of the topic is adequate. If you want to proof the soundness of a syntactic Hilbert style calculus, i.e. showing that $\Delta\vdash\alpha \...
1
vote
0answers
167 views
substitution lemmas for first order logic
How can i prove $ \text{$\models$}_{\Sigma} ((\forall x \ \varphi ) \ \Leftrightarrow \ (\forall y \ [\varphi]_{y}^{x}))$.
Being $ \Sigma $ a signature, $ \varphi$ a formula, and $ [\varphi]_{y}^{...
2
votes
2answers
174 views
Changing Hilbert-style axioms
Consider the following system for Hilbert-style deduction:
Axioms:
$A \rightarrow (B \rightarrow A)$
$(A \rightarrow (B \rightarrow C)) \rightarrow ((A \rightarrow B) \rightarrow (A \rightarrow C))$
$...
2
votes
1answer
1k views
Hilbert style proof of double negation introduction and reductio ab adsurdum
I'm trying to prove:
$\phi\to\neg\neg\phi$
$(\neg\phi\to\neg\psi)\to((\neg\phi\to\psi)\to\phi)$
Using these axioms with modus ponens and the deduction theorem:
A1: $\phi\to(\psi\to\phi)$
A2: $(\...
2
votes
0answers
80 views
Disproving completeness of an HPC-like proof system
Question
Given a new proof system S which contains the following axioms:
The regular HPC axioms (https://en.wikipedia.org/wiki/Hilbert_system) P1-P4.
A new axiom is introduced: $(a \lor b) \...
0
votes
0answers
37 views
Find a function $b$ such that the operator $\frac{d}{dx}+b(x)$ is symmetric with the weight $x^2$
Find the value of $b(x) \in \mathbb{C}, x\in \mathbb{R}$, so that $$Â=(Â^{*})^{t}$$ with
$$Â=i\frac{d}{dx}+b(x)$$
Here, $(f|g)$ is defined by
$$
\int_{-\infty}^{\infty} x^{2}f^{*}(x)g(x)dx
$$
I ...
7
votes
2answers
3k views
Difference between Logical Axioms and Rules of Inference
What's the difference between Logical Axioms and Rules of Inference? In my understanding, both are ordered pairs of formulas which are used to reach a conclusion through syllogisms.
My questions
...
10
votes
3answers
991 views
Difference between Gentzen and Hilbert Calculi
What is the difference between Gentzen and Hilbert Calculi?
From my understanding of Rautenberg's Concise Introduction to Mathematical Logic, Gentzen calculus is based on sequents and Hilbert ...
2
votes
1answer
68 views
Hilbert Calculus, Formal Proof Converse
I'm trying to find a proof of $\exists x\phi\rightarrow\exists y\phi^x_y$ in the Hilbert-calculus while working through a completeness proof for FOL on my own. Can anyone provide a proof of this ...
2
votes
2answers
90 views
Prove using Hilbert calculus $\forall x(Px\rightarrow x\equiv a)\vdash Pb\rightarrow Pa$, formal proof.
Prove: $\forall x(Px\rightarrow x\equiv a)\vdash Pb\rightarrow Pa$ Using Hilbert Calculus
Format of solution: Step (my understanding)
Solution:
(1) $\forall x(Px\rightarrow x\equiv a)\vdash Pb\...
