Tag Info

Accepted

Proving $\vdash \neg \neg P \to P$ (double negation elimination) in first order logic, preferrably without deduction theorem

First, here is proof that shows $\neg \neg P \vdash P$: \begin{array}{lll} 1&\neg \neg P & Premise\\ 2&\neg \neg P \to (\neg \neg \neg \neg P \to \neg \neg P) & Axiom \ 1\\ 3&\neg ...
• 99.3k
Accepted

What is the motivation for the axioms for Propositional Calculus in Mendelson's "Introduction to Mathematical Logic"?

I always think of the first axiom as a kind of Conditionalization: $P$ $\therefore Q \to P$ Conditionalization allows you, in effect, to bring results inside a certain context. That is, once we know ...
• 99.3k

What is the motivation for the axioms for Propositional Calculus in Mendelson's "Introduction to Mathematical Logic"?

Hilbert himself cites the relevant axioms as follows (see his The Foundations of Mathematics in From Frege to Gödel: A Source Book in Mathematical Logic, 1879-1931 edited by Jean van Heijenoort, ...
• 2,176
Accepted

• 57.9k
Accepted

Relationship between sequent calculus and Hilbert systems, natural deduction, etc

To define a logic you need to specify a language of formulas, and then you need to provide either 1) a semantics, or 2) a proof system (i.e. a collection of rules of inference). For commonly ...
• 24.9k
Accepted

• 16.7k
Accepted

Derive $P \to \neg \neg P$ in a structure with not and implies

Yes, this is possible, but the proof is not short and simple. From a birds-eye view, the trick is to start by proving double-negation elimination: $$\neg\neg Q \to Q$$ This requires two instances of ...

theoretical question regarding deduction and relation between $\vdash$ and $\vDash$

You have to prove a sort of soundness theorem for your calculus. Hint about soundness : if $\Gamma \vdash a$, the $\Gamma \vDash a$. Assume that $\Gamma \vdash a$ and consider the ususal cases : ...
• 93.8k
Accepted

How to prove $\lnot (\alpha \rightarrow \lnot \beta) \vdash \lnot (\beta \rightarrow \lnot \alpha)$ in HPC

Assuming you can use the Deduction Theorem, I would follow the following path: First, prove: $$\neg \alpha \rightarrow (\alpha \rightarrow \beta)$$ Combine this with the following instantiation of ...
• 99.3k

• 93.8k
Accepted

• 99.3k
Accepted

Proofs using theorems instead of axioms

Now that we have the source of your problem, we can help you... See: Moshe Machover, Set Theory, Logic and Their Limitations Cambridge UP (1996), page 116-on for the definitions and some results ...
• 93.8k
Accepted

Can we prove if ⊢ (α → β) and ⊢ (¬α → β) then ⊢ β in L0?

Yes, we can, but it's a bit of work! (well, I myself couldn't find any shorter way ...) First, let's prove: $\phi \to \psi, \psi \to \chi, \phi \vdash \chi$: $\phi \to \psi$ Premise $\psi \to \chi$ ...
• 99.3k
Accepted

can we a prove ⊢ (α → α) → (α → α)

Here is a proof of $\alpha \to \alpha$: \begin{array}{lll} 1 & (\alpha \to ((\alpha \to \alpha) \to \alpha) \to ((\alpha \to (\alpha \to \alpha)) \to (\alpha \to \alpha)) &A2\\ 2 & \alpha ...
• 99.3k

What is the probability of randomly generating a tautology?

Nice question! I doubt that you'll find a closed form for arbitrary $n$, but I'll solve it for $n=1$, and higher values of $n$ could be treated analogously with more effort. Classify the formulas ...
• 236k
Accepted

What is the proof of reductio ad absurdum (RAA) in a Łukasiewicz axiom system for propositional logic with only modus ponens?

So you want to prove the following theorem: Theorem: If $\Gamma,\phi \vdash \psi$ and $\Gamma, \phi \vdash \neg \psi$, then $\Gamma \vdash \neg \phi$ Proof: First, I'll assume that you can use the ...
• 99.3k

Do inference rules mean the same in a Hilbert system and in a natural deductive system?

Do inference rules mean the same in a Hilbert system and in a natural deductive system? YES. See Rule of inference. The "canonical" representation is quite standard, but it is only a ...
• 93.8k
Should $\vdash$ in Theorem 24B In Enderton's logic book be $\models$ instead?
As spaceisdarkgreen says, there is no typo here: Enderton means "$\vdash$" in the theorem, and "logical entailment" ($\models$) in the remark. The remark observes that there is a ...
Note: This answer works with $\neg,\to$ as the base connectives, the word "calculus" always refers to a Hilbert-style proof calculus for propositional logic.The system presented in Mendelson ...