Questions tagged [proof-theory]
Proof theory is an area of logic that studies proof as formal mathematical objects. If you'd like advice on the presentation of a proof you have in draft, use proof-writing instead. If you'd like feedback on its validity, use proof-verification. If none of the above apply, you do not need a proof-* ...
-1
votes
1answer
68 views
Can all proven theorems be proven by contradiction?
The answers to the question Can every true theorem that has a proof be proven by contradiction? show that if a theorem can be proven directly, it can be proven by contradiction.
The main arguments ...
-3
votes
1answer
51 views
Is there a statement which can not be proved in any axiom systems
As we know a statement may not be proved in some axiom system according to the godel incompleteness theory, can we always solve it by some way that change the axiom system?
2
votes
0answers
87 views
Translating from First Order Logic to Order-Sorted Logic
The following single sorted FOL sentences are from Stanford. Sorts or types are represented by predicates (e.g. $Horse(x)$)
\begin{align*}
&(1a) \forall x, \forall y ((Horse(x) \land Dog(y)) \...
2
votes
1answer
47 views
Exercise 2 (p. 30) on W. Rautenberg - A concise introduction to Logic.
I'm can't solve Exercise 2 on page 30 on Rautenberg (Chapter 1.4 - A calculus of Natural Deduction), which reads:
Augment the signature $\{\lnot, \land\}$ by $\lor$ and prove the completeness of the ...
-4
votes
2answers
47 views
How does one prove that there are no more solutions to an equations than the ones already found? [closed]
For example, I had the following equation:
$ $
$x^2-148x+576=0$
$⇔ (x-4)(x-144)=0$
$⇔ x=4 ∨ x=144$
$ $
How do I prove that these two are the only possible solutions (without the use of ...
2
votes
2answers
98 views
Doubts about Goedel Completeness Theorem
My book (Mendelson) states this theorem the following way:
(1) A logically valid formula of a first order theory is a theorem.
On Wikipedia the statement is a little more general:
(2) For any ...
2
votes
1answer
180 views
About proofs by contrapositive and proofs by contradiction
I'm a little confused about the difference between these two types of proof. As I have been taught them, it seems like proofs by contrapositive are just a subset of proofs by contradiction.
Say we ...
0
votes
2answers
40 views
Induction proof inequality
So I got this induction proof question but I can't seem to make a logical statement in one part of it:
The question is , $a_{n + 1} = 5 - \frac{6}{a_n + 2}$ with
$a_1 = 1$ . Prove by induction that ...
21
votes
10answers
3k views
What exactly is circular reasoning?
The way I used to be getting it was that circular reasoning occurs when a proof contains its thesis within its assumptions. Then, everything such a proof "proves" is that this particular statement ...
1
vote
1answer
52 views
Independence and Consistence of Formal Systems
Let $S$ be a formal system with axioms $A,A_1,\dots,A_n$. The system $S$ is said to be consistent if no contradiction can be proved (i.e. we can’t prove both a formula and its negation). If $S$ is ...
4
votes
1answer
139 views
Curry-Howard for an imperative programming language?
The Curry-Howard isomorphism links proofs of propositions, with "programs" and types.
But the way I am introduced to it, "programs" is interpreted in a functional way, i.e. in lambda calculus with ...
5
votes
1answer
99 views
Why can't we generally replace inference rules with axioms?
Is there a big difference in having insufficient axioms and insufficient inference rules/proof procedure to have a complete theory?
It seems like in many cases adding a new inference rule or a new ...
2
votes
0answers
74 views
Paradox,shortest proof
I have read somewhere that the shortest proof of a certain formula in the language of natural numbers contains some kind of paradox. I cannot remember what this paradox was nor where I've read it. It ...
2
votes
1answer
24 views
sequent calculus for first order logic
I've just started learning sequent calculus. Now I'm trying to prove the formula below:
$$ \exists x (P → Q) ⊨ P → \forall x Q $$
My approach to the problem:
$$ \underline{_⊢\exists x (P → Q) , _⊣ P ...
1
vote
2answers
123 views
Axioms of propositional logic
The book on which I'm studying logic (Mendelson) uses the following axioms:
$$\begin{array} {rl}
\text{A1)} & P \to (Q \to P) \\
\text{A2)} & [P \to (Q \to R)] \to [(P \to Q) \to (P \to R)...
0
votes
1answer
65 views
What does this proof mean?
I'm having difficulty reading these proofs,
Definition 1 $V$ is an NP-verifier for $L$ if $V$ is polynomial-time in the length of the first input and that the following two properties hold:
...
1
vote
2answers
49 views
universal instantiation and the Archimedean property
I have been under the impression that I could substitute just about anything for the variables in any proven theorem (via universal instantiation logic rule) but when applied to the Archimedean ...
0
votes
0answers
19 views
When are (hyper)cubes used instead of balls as the basic constructs to argue for “whole” spaces?
When are (hyper)cubes used instead of balls as the basic constructs to argue for "whole" spaces?
Like e.g. when one wants to prove smoothness properties through induction (prove for unit ball $\...
5
votes
3answers
534 views
Defining new symbols in a proof, when is this justified?
So I have a proof that I have written of $X\subset Y \Rightarrow f(X)\subset f(Y)$ but it is slightly different than the one presented in this questions accepted answer.
The difference is subtle so ...
2
votes
1answer
40 views
Proof theory outside of structural proof theory (calculi)?
Is there proof theory for some more or less usual logics that is outside the scope of structural proof theory (Hilbert/natural deduction/sequent calculi)? E.g. proof theoy for adaptive logic (https://...
4
votes
3answers
129 views
Is there a type of mathematical proof besides direct, counterpositive and absurd?
When proving a mathematical statement $p \Rightarrow q$, we normally do it:
1) Assuming $p$, then showing $p \Rightarrow q$ (Direct proof)
2) Assuming $¬q$, then showing $¬q \Rightarrow ¬p$. (...
1
vote
0answers
52 views
Applying the necessitation rule in semantic tableaux
I have a question about the necessitation rule in normal modal logics. Using an axiomatic system, once I proved $P$ I can apply necessitation and prove that $P$ is necessary ($\Box P$). In tableaux, ...
1
vote
1answer
66 views
Given a new proof system N show that…
Defining the new proof system $N$ as this:
We have 2 Axioms -
$$A \rightarrow (A \lor B)$$
$$A \rightarrow (B \rightarrow A)$$
A new deduction rule:
$$\bullet \frac{(A \rightarrow B)}{A \rightarrow (...
0
votes
1answer
32 views
Maximal (or prime) theories and their sets
Probably it is very simple lemma but I cannot see it. Suppose that we have intuitionistic propositional logic (in fact, it can be classical) and $W$ is the set of all prime (or maximal - in classical ...
4
votes
1answer
69 views
What is a heuristic proof?
I just wonder what does a heuristic proof approach really means. I keep finding it in books and from teachers. I got to the next analogy:
A heuristic proof of a mathematical proof is like pseudo-...
2
votes
3answers
62 views
Explaining the resolution rule.
It is nice to have inference rules explained informally. For example, the rule of Disjunctive Syllogism $((x \lor y) \land \neg y)\rightarrow x$ can be explained as follows: since $x \lor y$ is true, ...
1
vote
1answer
37 views
A axiomatization of (full) Second Order Logic with a decidable proof system cannot be complete; is this true if we only require semi-decidability?
My understanding is that, unlike first order logic, no "effective" (sound, consistent) axiomatization of second order logic is complete; there will always be statements true in all models, but not ...
0
votes
1answer
97 views
Provably unprovable statement?
Suppose we have a consistent axiomatizable theory $T$ extending the theory of $A_E$ where $A_E$ are these axioms (slide 5 here). Can we find some sentence $\varphi$ such that $T$ proves that it doesn'...
0
votes
1answer
38 views
How to prove statements in formal set theory? Substitution, the empty set and an example.
I would like to better understand how to formally prove a statement in the first order axiomatic set theory or ZFC. One example of an axiomatization can be found here.
There are a few issues. First, ...
1
vote
0answers
29 views
Is it possible to give a Henkin-style completeness proof for tableaux systems?
My question is: Is it possible to give a Henkin-style completeness proof for tableaux systems instead of the usual Hintikka-style one?
By Henkin-style, I mean that the proof involves extending ...
0
votes
1answer
50 views
How to show local soundness and completeness for NAND
I have been following Frank Pfenning's Notes on natural deduction, and I have a few questions on how to write rules with the local soundness and local completeness properties.
Consider these rules ...
0
votes
1answer
41 views
Can second order peano arithmetic prove that first order peano arithmetic is sound? [closed]
Can second order peano arithmetic prove that first order peano arithmetic is sound?
Note that I'm not just talking about its axioms, but also its theorems.
2
votes
0answers
25 views
Uniqueness of realizers
This is a pretty basic question about realizability interpretations. I am just starting to learn this subject so hopefully this question makes sense, please feel free to improve it. It seems that ...
1
vote
0answers
50 views
For every formula of linear logic, is there an equivalent formula in intuitionistic linear logic?
Consider the sequent calculus presentations of propositional linear logic (LL) and propositional intuitionistic linear logic (ILL). Clearly, there are formulas in LL that are not in ILL, such as $\bot$...
6
votes
2answers
89 views
Can two different models of arithmetic have non-comparable views of peano arithmetic?
For a given model of arithmetic $M$, we say that models view of peano arithmetic, $V(M)$, is $\{\phi : M \models (PA \vdash \phi) \}$.
For example the view of the standard model is $\{\phi : PA \...
3
votes
1answer
315 views
How can we be so sure that we don't live in Pudlak's inconsistent world?
In his Logical Foundation of Mathematics and Computational Complexity (2013), Pavel Pudlak invites the readers to ponder about fictitious people whose natural numbers are nonstandard. His exposition ...
22
votes
7answers
6k views
Why does proof by elimination work?
I get that if all the other options are proven wrong, then the only option left must be the correct option. But why does this work? What is the logic behind it? It just doesn't click with me for some ...
-1
votes
1answer
60 views
If Algorithms Count as Formal Proofs
From my understanding, for proofs to be considered "formal" as opposed to social/casual, they need to be computable or at least be a set of transformations of strings of symbols. By algorithm I mean ...
1
vote
0answers
35 views
How is this HA unprovable formula recursive realizable?
In Realizability: A Historical Essay [Jaap van Oosten, 2002], it is said that recursive realizability and HA provability do not concur, because although every HA provable closed formula is realizable, ...
1
vote
1answer
118 views
What is a construction (in mathematics)?
Related questions: Formally what is a mathematical construction? and What is a Universal Construction in Category Theory?
Backstory: A question arose in a seminar that concluded with the statement ...
3
votes
3answers
102 views
Comma in turnstile (entailment)
In a sequent, on the left and right-hand side of the turnstile operator, does the comma denote disjunction or conjunction?
$$\frac{...}{\Delta_1,\Delta_2 \vdash \Gamma_1,\Gamma_2}$$
I think it's one ...
2
votes
1answer
93 views
Why does this theory prove that it's not consistent?
Say we have some theory $T$ such that $Th(A_E) \subseteq T$ where $A_E$ are the axioms of arithmetic. How do I show that
(1) there are sentences $\varphi_1$ and $\varphi_2$ such that $Th(A_E) \vdash ...
10
votes
1answer
1k views
Is it a paradox if I prove something as unprovable?
The Goldbach Conjecture asserts:
It is possible to write every even number greater that 2 as the sum of
two primes.
Assume I can prove that the Goldbach Conjecture is unprovable from the Peano ...
0
votes
1answer
48 views
How to formally prove $\forall x: x11=x$ in the theory of groups.
Def 1: $M$ is a $\underline{theory}$, if it is a collection of first order statements.
Def 2: Given theory $M$ and first order statement $\phi$, then $M$ can $\underline{prove}$ $\phi$ if, starting ...
1
vote
0answers
49 views
Reference request for a formalized and organized take on the foundations (logic and set theory)
For over 8 months, I have been actively looking for a resource that rigorously tackles mathematical logic - at the same level described in this lecture, timestamp 56:09. A resource which minds the ...
1
vote
1answer
40 views
Is an induction inside of an induction allowed in a proof?
Note: I'll be putting letters before each statement I discuss in order to easily reference them.
If I'm proving a statement with induction, can I use induction on a statement that I derive inside ...
2
votes
1answer
59 views
Original purpose of Fundamental Sequences of limit ordinals
I am curious of why fundamental sequences of limit ordinals were invented? Was it only to be able to define a function (e.g. fast-growing) hierarchy?
For instance:
Zero ordinal 0: $f_{0}(n) = n + 1$
...
0
votes
1answer
28 views
How sequent calculus are connected with the usual notion of satisfiability or validitiy of formula?
I know the notions "satisfiablity", "validity" and "consequence" as applied to the logic, e.g. First Order logic https://en.wikipedia.org/wiki/First-order_logic#Validity,_satisfiability,...
-1
votes
1answer
38 views
Is the Proof Mathematical Object as a Function?
While I am discussing over the definition of the proof with my friends, one says
"proof is definitely a mathematical object which maps a formal representation of mathematical objects into two ...
1
vote
1answer
46 views
Natural Deduction - 'monotone' property of sequent
In natural deduction, what says that the following is correct?
$\Gamma \Rightarrow B$ then $ \Gamma, A \Rightarrow B$
I saw a proof that uses this rule without mentioning it and I can't find the ...
