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-* tag.
1,050 questions
0
votes
0
answers
85
views
Is there a definition for stronger independence of a proposition concerning an axiomatic system.
I wonder if a definition like the following already exists.
If we have an axiom set $A$, can we define the independence of $\alpha$ in the situation where we are adding a new axiom $\alpha$ to $A$ ...
- 421
0
votes
1
answer
83
views
Is there a complete proof system for deriving some axiom schema from others?
Say that an axiom schema is an algorithm $A$ that produces a family of first-order statements (I believe we can recursively enumerate all the algorithms that produce well-formed sentences). Given ...
- 2,625
2
votes
1
answer
127
views
Constructively weaker versions of well-order, well-foundedness and so on
I have heard that, from a constructive point of view, it is quite difficult to show that a given order $X$ is a well-order, i.e. each subset of $X$ has a minimum, or better constructivley $\forall_x(\...
- 309
4
votes
0
answers
90
views
Prenex normal forms in intuitionistic logic
In classical logic each formula can be rebuilt to an equivalent prenex normal form. In intuitionistic logic the algorithm fails, since
$\forall x(P(x)\vee R)\not\vdash\forall xP(x)\vee R,$
$\forall ...
- 1,527
-2
votes
2
answers
436
views
Can it be proved that $\mathbb{N}\subseteq e$ if we can prove $0\in e$, $1\in e$, etc. separately?
Suppose for every natural number $n$, $Z_n(x)$ is a first order predicate with a single free variable $x$ that states, informally, that $x = n$. For instance $Z_0(x)$, stating that $x = 0$, i.e. that $...
- 12k
2
votes
2
answers
225
views
Is there an infinite sequence of countable models of ZFC such that each believes its predecessors are countable?
If ZFC is consistent, then by Löwenheim–Skolem, there exist countable models of ZFC. Since this is a theorem of ZFC, it would seem to hold in every model, even a countable one. But each model believes ...
- 1,843
6
votes
1
answer
126
views
What does it mean for two theories to have the same proof theoretic strength?
In the paper by Rathjen it is stated that that CZF + Inacc(n) for all n > 0 and MLTT have the same proof theoretic strength. According to other sources the ordinal assigned to each of these ...
- 281
1
vote
0
answers
112
views
Where is the relativized uniform complementor on r.e. indices stated explicitly (index-operator form)—existence for $\emptyset'$ and any minimality?
Let $\langle W_e : e\in\mathbb{N}\rangle$ be the standard effective enumeration of recursively enumerable (r.e.) sets, where
$$
n\in W_e \;\Longleftrightarrow\; \exists s\;\big(\varphi_e(n)\ \text{...
- 31
4
votes
1
answer
79
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
1
vote
1
answer
144
views
Does there exist a sequence of all theorems of Peano Arithmetic with this property?
Does there exist an infinite sequence of all theorems of Peano Arithmetic, with no repeats, such that for any positive integer $n$, the finite subsequence from $1$ to $n$ is a proof of the theorem at $...
- 24.9k
3
votes
0
answers
164
views
Asymptotic structure of random theories in logic
Fix a first-order language L. Consider all possible sets of contingent sentences of length less than or equal to n in L. Dispose of the inconsistent such sets, then from the remaining collection, ...
user1286971
3
votes
2
answers
186
views
Can we prove $P(\varepsilon x \top) \leftrightarrow P(\varepsilon x\bot) \leftrightarrow \forall xP(x)$ in Hilbert's epsilon calculus?
Can we prove $P(\varepsilon x\top)\leftrightarrow P(\varepsilon x \bot)\leftrightarrow\forall xP(x)$ in the epsilon calculus?
I expect these statements to be true, since in the case $\varepsilon x\top$...
- 133
3
votes
0
answers
128
views
Is there a sense in which a proof defines an algorithm?
As I get further into undergrad I have begun to wonder more and more if proofs essentially define an algorithm. It seems like in general, proofs are of the following form: "given an object(s) or ...
- 335
-1
votes
2
answers
188
views
Replacing axiom schema $(\bot \rightarrow A)$ in Hilbert system
This is exercise 2.4.2C, page 54 from Basic Proof Theory by Troelstra:
Show that Hi with $\neg$ as primitive operator may be axiomatized by replacing the axiom schema $\bot \rightarrow A$ by $A \...
- 61
3
votes
2
answers
245
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