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

51 questions
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 ...
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)...
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 ...
82 views

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$. ...
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 ...
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$$ ...
70 views

121 views

64 views

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)$ ...
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 ...
184 views

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.
142 views

247 views