Questions tagged [formal-proofs]
For questions about proofs within a formal system, such as natural deduction or Hilbert system.
867 questions
3 votes
1 answer
70 views
Can We Prove the Completeness of Propositional Logic also with Structural Induction?
In propositional logic, the "semantics" $v[\![\varphi]\!]$ of a formula $\varphi$ with respect to some valuation $v$ is defined inductively on the syntactic structure of the formula $\varphi$...
- 43
0 votes
0 answers
45 views
What is philosophically the distinction between using a theory to study itself and Godel-like sentences?
Contructions involving Godel-numbers allow a sufficiently expressive theory to talk about itself, i.e. there is a correspondence between sentences in the theory and sentences about the theory. There ...
- 1,679
2 votes
1 answer
141 views
Can first-order logic prove "theorem schemas"?
Examples of "axiom schemas" are well known, e.g. Replacement in ZFC. The notion I have of "theorem schema" is an analogous notion, i.e. an infinite collection of (non-axiom) ...
- 2,303
4 votes
1 answer
78 views
Proof of deduction with only atomic consequences of $\bot_C$
I am reading Dag Prawitz's "Natural Deduction: A Proof-Theoreritcal Study" and am confused by the proof of Theorem 1, Chapter 3 that: If $\Gamma \vdash_{\mathsf{C}'} A$, then there is a ...
- 43
4 votes
2 answers
174 views
Formally prove that $\phi\rightarrow \psi \vdash \neg \psi \rightarrow\neg \phi$ in Hilbert system
In the book Gödel's Theorems and Zermelo's Axioms by Halbeisen and Krapf the first chapter contains an excercise that asks us to prove $$\phi\rightarrow \psi \vdash \neg \psi \rightarrow\neg \phi,$$ i....
- 173
0 votes
0 answers
131 views
Turning “morally $X=Y$” into a rewrite rule (Lean/Coq/Agda)
By “morally $X=Y$” I mean a canonical equivalence in context rather than judgmental equality. In a proof assistant (e.g., Lean/...
user1675092
3 votes
2 answers
239 views
Understanding Rosser's trick in a self-referential system
This is a follow-on from this question talking about how adding a self-referential axiom, $\varphi\leftrightarrow Con(\mathsf{PA}+\varphi)$ to PA interacts with Godel's theorems. Noah Schweber answers ...
- 738
4 votes
3 answers
491 views
Why assume first-order logic can formalize all mathematical reasoning?
In thinking about the years circa 1900 when people were first seriously attempting the formalization of mathematics (e.g. via a formal logic like Frege’s or Whitehead & Russell’s), it seems like ...
- 2,303
2 votes
3 answers
166 views
Proving the following distributive law of $\rightarrow$ over $\vee$: $[p \rightarrow (q \vee r)]\rightarrow [(p \rightarrow q)\vee(p \rightarrow r)]$
$[p \rightarrow (q \vee r)]\rightarrow [(p \rightarrow q)\vee(p \rightarrow r)]$ I am having trouble proving this, I proved it the other way around. I am using the rule in the open logic calculator. ...
- 6,902
4 votes
3 answers
466 views
Prove that the following formula is a theorem in natural deduction
Prove that the formula $$\exists x\, (\neg r(x) \lor q(x)) \rightarrow (\forall x\, (p(x) \land r(x)) \rightarrow \exists x\, (q(x) \land p(x)))$$ is a theorem in natural deduction. The formula I ...
- 377
0 votes
0 answers
90 views
Some questions about a formal proof of Euler-Maclaurin formula
$\quad$ In the course of mathematical analysis,we usually need to deal with some infinite series or expressions including transcendent functions.And one of most important things is to get their ...
- 19
0 votes
1 answer
143 views
Using the Frege-Lukasiewicz axioms and Inference Rules for prove $P \to Q, \neg Q \vdash \neg P$
¡Hi! I am studying logic from the book First Course in Mathematical Logic and Set Theory by Michael L. O'Leary and trying to do some exercises that require only the use of the Frege-Łukasiewicz axioms ...
1 vote
1 answer
35 views
Symmetric Cuts on the Sides of a Triangle
Let $ABC$ be a triangle, and $a$ lie on $BC$, etc.. Given that $a$ cuts $BC$ in the proportion $k:(1-k)$, and $b$ cuts $CA$ in $l:(1-l)$, if $Cc$ passes through the intersection $Aa\cap Bb$, and cuts $...
- 1,839
4 votes
1 answer
239 views
Prove the invertibility of the "double negation" elimination rule for minimal logic
In the technical report his prover for Minimal logic, Slaney defined a rule that he called "double negation". He wrote: This looks surprising at first, since of course double negation ...
4 votes
1 answer
111 views
$\Gamma, \phi \vdash \theta$ and $\Gamma, \psi \vdash \theta$ yield $\Gamma, \phi\vee \psi \vdash \theta$?
I have a logical system similar to NJ (in fact it is an extension) and I have shown that $\Gamma, \phi \vdash \theta$ and $\Gamma, \psi \vdash \theta$. It seems relatively obvious that I can have $\...
