Search Results
Search type | Search syntax |
---|---|
Tags | [tag] |
Exact | "words here" |
Author |
user:1234 user:me (yours) |
Score |
score:3 (3+) score:0 (none) |
Answers |
answers:3 (3+) answers:0 (none) isaccepted:yes hasaccepted:no inquestion:1234 |
Views | views:250 |
Code | code:"if (foo != bar)" |
Sections |
title:apples body:"apples oranges" |
URL | url:"*.example.com" |
Saves | in:saves |
Status |
closed:yes duplicate:no migrated:no wiki:no |
Types |
is:question is:answer |
Exclude |
-[tag] -apples |
For more details on advanced search visit our help page |
first-order and higher-order logic, model theory, set theory, proof theory, computability theory, formal languages, definability, interplay of syntax and semantics, constructive logic, intuitionism, philosophical logic, modal logic, completeness, Gödel incompleteness, decidability, undecidability, theories of truth, truth revision, consistency.
33
votes
Interesting meta-meta-mathematical theorems?
In Reverse Mathematics, we can study what happens if we use weak systems of second-arithmetic as metatheories. For example, we can study the strength of the completeness theorem and prove results such …
28
votes
Accepted
Complete mathematics
You probably intended to restrict the question to effectively axiomatizable theories. Otherwise, for example, the first-order theory of the standard model of arithmetic is a complete theory, as is the …
26
votes
Accepted
Deduction theorem
Failures of the deduction theorem are one of the more mysterious topics in logic, in my experience. The motto is that axioms are stronger than rules.
Here is the simplest nontrivial example that I k …
25
votes
Accepted
What is "Seetapun Enigma"?
The question seems to be about the following special form of Ramsey's Theorem:
$\mathsf{RT}^2_2$: for every $2$-coloring of the unordered pairs from $\mathbb{N}$ there is an infinite subset of $\m …
24
votes
Accepted
Induction vs. Strong Induction
The terms "weak induction" and "strong induction" are not commonly used in the study of logic. The terms are commonly used only in books aimed at teaching students how to write proofs.
Here are thei …
23
votes
Accepted
Clarification of Gödel's second incompleteness theorem
The key idea Feferman is exploiting is that there can be two different enumerations of the axioms of a theory, so that the theory does not prove that the two enumerations give the same theory.
Here i …
22
votes
Why are proofs so valuable, although we do not know that our axiom system is consistent?
Gödel's theorems do not say that we can never know our axiom systems are consistent. Not at all. What they say is that we can never prove that certain systems are consistent within those systems thems …
22
votes
Accepted
Second-order term in first-order logic?
I think that the spirit of this question, combined with the clarifications in comments, is:
What is it that makes first-order logic "first order"?
Unfortunately, the terms "first order" and "se …
22
votes
Accepted
Can we prove set theory is consistent?
Would you accept it if Set1 just proved the existence of a model for Set2 (in the same way that Set1 proves the consistency of formalized Peano arithmetic by providing a model of it)?
If so, and if y …
20
votes
Decidable but nonrecursive sets
In the field of computability theory, the terms "decidable set", "computable set", and "recursive set" are all formally defined and they all mean the same thing. So, to put it gently, Wells is misusi …
20
votes
Proving Independence of Axioms by Exhibiting Models Which Don't Satisfy Our Intuition
You have run into one of the main themes of contemporary logic: the difference between "truth in the standard model" and "provability". This is an extremely deep issue, so I'm sure other people will a …
19
votes
Are all functions in Bishop's constructive mathematics continuous?
Bishop's mathematics is compatible with classical mathematics. For example, if we look at set theory in Bishop's framework, each model V of ZFC is a model of Bishop's system, and if we look at second- …
18
votes
Accepted
Undecidable theories easier than $Q$
When I was looking around trying to find some inspiration to answer your question, I found the following result of Feferman from 1957:
For any set $X$ of natural numbers there is a theory $T(X)$ s …
17
votes
Can infinity shorten proofs a lot?
The axiom system PRA of "primitive-recursive arithmetic" is finitistic, but it has been known for a few decades that it has the same set of $\Pi^0_1$ consequences as the infinitistic theory $\text{WKL …
15
votes
Accepted
Ackermann function in the Primitive recursive arithmetic
You can express the totality of any computable function in PRA, using Kleene's T predicate, which is primitive recursive. So if you pick any index $e$ for the Ackermann function, the formula $(\forall …