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.

27 questions with no upvoted or accepted answers
Filter by
Sorted by
Tagged with
3
votes
2answers
62 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) ...
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 ...
2
votes
1answer
149 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 ...
2
votes
0answers
55 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 ...
2
votes
0answers
88 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) \...
2
votes
1answer
195 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 \...
1
vote
0answers
30 views

Reference for proof of completeness of classical predicate logic in a Hilbert system

Many proofs of the completeness of classical logic with respect to some particular Hilbert style atomization of it do not explicitly reference the axioms at hand. The devils must be buried in the ...
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 ...
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(...
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 ...
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 $ ...
1
vote
0answers
79 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
0answers
68 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
vote
0answers
104 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
68 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
0answers
273 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}^{...
0
votes
0answers
18 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 ...
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
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 ...
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
52 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)...
0
votes
1answer
39 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 (...
0
votes
0answers
144 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$$ ...
0
votes
1answer
144 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. ...
0
votes
0answers
38 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 ...
-1
votes
1answer
91 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 ...