10 votes
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 ...
Bram28's user avatar
  • 99.3k
10 votes
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 ...
Bram28's user avatar
  • 99.3k
9 votes

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, ...
Tankut Beygu's user avatar
  • 2,176
8 votes
Accepted

Hilbert style proof of double negation introduction and reductio ab adsurdum

A) 1) $\lnot \lnot \lnot \phi \to \lnot \phi$ --- from $\lnot \lnot \phi \to \phi$ 2) $(\lnot \lnot \lnot \phi \to \lnot \phi) \to (\phi \to \lnot \lnot \phi)$ --- Ax.3 3) $\phi \to \lnot \lnot \...
Mauro ALLEGRANZA's user avatar
8 votes
Accepted

How can we prove soundness property if it's possible for our assumption set to contain false assumptions?

If $\bot\in \Gamma,$ then we have $\Gamma\vdash \bot$ and $\Gamma \models \bot,$ so this is not in conflict with the soundness theorem. It is clear that $\Gamma \vdash \bot.$ The reason $\Gamma \...
spaceisdarkgreen's user avatar
7 votes
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 ...
Derek Elkins left SE's user avatar
7 votes
Accepted

How to prove $((A \to B) \to A) \to A$ using Lukasiewicz's axioms, MP and deduction theorem?

The statement is known as Peirce's Law, and the proof is pretty nasty. I can believe someone can spend $10$ years on it without cracking it! The proof uses some helpful Lemma's. First, let's prove: $...
Bram28's user avatar
  • 99.3k
7 votes
Accepted

Is this Hilbert proof system complete?

This is not complete. To show it is not complete, let us consider an alternative semantics for the operators involved. That is, suppose that all statements involved evaluate to either $0$, $1$, or $2$....
Bram28's user avatar
  • 99.3k
6 votes
Accepted

Hilbert System Logical Axiom 1 follows from Axioms 2 and 3

Hint: Remember you get to pick what $\psi$ is. Is there any formula $\psi$ such that you know $(\phi\to\psi)$ is true? More details are hidden below.
Eric Wofsey's user avatar
6 votes
Accepted

strong completeness of a formal system

No, the system $D$ is not strongly complete. Indeed, consider the formula $((X \to Y) \to X) \to X$ where $X$ and $Y$ are propositional variables. It is immediate to verify that $\models ((X \to Y) \...
Taroccoesbrocco's user avatar
5 votes
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 ...
hmakholm left over Monica's user avatar
4 votes

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 : ...
Mauro ALLEGRANZA's user avatar
4 votes
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 ...
Bram28's user avatar
  • 99.3k
4 votes

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

The other answers show how to prove $P\to P$ and then set $P\equiv(\alpha\to\alpha)$. This works, of course. But your particular goal can be reached faster with the axioms you have: $(\alpha\to(\...
hmakholm left over Monica's user avatar
4 votes
Accepted

What are the restrictions on substitution of terms in Hilbert-style calculus vis-à-vis intuitionistic logic?

Just because $((C \rightarrow B) \rightarrow B) \leftrightarrow C$ can't be proven in general doesn't mean it can't be proven for particular values of $B$ and $C$. The problem is that you have the ...
SCappella's user avatar
  • 2,516
4 votes

Hilbert System Logical Axiom 1 follows from Axioms 2 and 3

By (3) we have $$ (\phi\to((\phi\to\phi)\to\phi))\to((\phi\to(\phi\to\phi))\to(\phi\to\phi)) $$ By (2), $$ \phi\to ((\phi\to\phi)\to\phi) $$ So $$ ((\phi\to(\phi\to\phi))\to(\phi\to\phi)) $$ by Modus ...
Reveillark's user avatar
4 votes

Prove the introduction of conjunction using axioms in a Hilbert system

Hint What you have to prove is: $(\alpha \to (\beta \to \lnot (\alpha \to \lnot \beta)))$. In order to do this, you have to prove negation introduction: $(\phi \to \psi) \to ((\phi \to \lnot \psi)...
Mauro ALLEGRANZA's user avatar
4 votes
Accepted

Prove double negation introduction with this axiom system.

By modus ponens, we see $$A, (A \to \bot) \vdash \bot$$ Then applying the deduction theorem twice, we find $$ \vdash A \to (A \to \bot) \to \bot$$ Lastly, we apply axiom $4$ twice to see $$ \vdash A \...
HallaSurvivor's user avatar
4 votes
Accepted

Axiomatic derivation - what does instancing an axiom practically entail?

That makes sense to me: if $p$ is true then $p$ is true. I recognise that $\phi\to(\psi\to\phi)$ is a tautology, it is technically true for every two propositions regardless of whether they are ...
Vsotvep's user avatar
  • 6,113
3 votes
Accepted

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.

Given a (possibly empty) set of formulas $\Delta$, a derivation of $\Delta \vdash A$ in a Hilbert system is also a derivation of $\Delta \cup \Gamma \vdash A$ in such Hilbert system, for any set of ...
Taroccoesbrocco's user avatar
3 votes

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

Is it possible to prove this? :-- $$P\to \lnot\lnot P$$ The person who gave me this problem insists it is provable, although it seems to me that such a proof is impossible, as none of the axioms ...
Bram28's user avatar
  • 99.3k
3 votes
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 ...
Mauro ALLEGRANZA's user avatar
3 votes
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$ ...
Bram28's user avatar
  • 99.3k
3 votes
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 ...
Bram28's user avatar
  • 99.3k
3 votes

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 ...
joriki's user avatar
  • 236k
3 votes
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 ...
Bram28's user avatar
  • 99.3k
3 votes

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 ...
Mauro ALLEGRANZA's user avatar
3 votes

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 ...
Noah Schweber's user avatar
3 votes

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

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 ...
Vivaan Daga's user avatar
  • 5,503

Only top scored, non community-wiki answers of a minimum length are eligible