Stack Exchange Network

Stack Exchange network consists of 175 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.

Visit Stack Exchange

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\...