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.
4
votes
Accepted
Proof formalization
In general, "formalising mathematical vernacular" is a good source for work relevant to your question. The field generally started in earnest with de Bruijn's Automath project.
Harvey Friedman has do …
4
votes
1
answer
871
views
Derivability conditions for Robinson arithmetic
Two pieces of hearsay I have encountered about Robinson's Q:
Q fails to satisfy the Löb derivability conditions;
Pudlák criticised the Löb derivability conditions and suggested rival, weaker conditi …
7
votes
Accepted
Is there a relationship between model theory and category theory?
Between model theory and category theory broadly conceived: not anything really compelling, because a category, on its own, does not stand as an interpretation for anything.
Between model theory and …
8
votes
Do you know any good introductory resource on sequent calculus?
Gentzen, 1934, 'Investigations into Logical Deduction' — This is very readable, and introduces so many ideas that later synthetic works invariably miss some. If you're serious, this, and some other p …
10
votes
2
answers
2k
views
Scott on the consistency of the lambda calculus
I have twice heard it attributed to Dana Scott that he said something to the effect that the consistency of the lambda-calculus was an accident.
Does anyone have a reasonable-sounding source for this …
5
votes
When is something too big to be a set?
I find the terminology of "too big" to be misleading. I think it comes about from thinking that the strength of a set theory comes from the generosity of its comprehension axioms, that stronger set t …
9
votes
Most general formulation of Gödel's incompleteness theorems
Theories can be be represented recursion-theoretically by an encoding of the language as natural numbers (most simply, a bijective encoding, which I assume), and a Turing machine that accepts all and …
7
votes
Accepted
Weakest subsystems of second order arithmetic for mathematical logic
In fact, the incompleteness and completeness theorems can be proven in subsystems of second-order arithmetic weaker than RCA-0: incompleteness can be proven in EFA (first-order elementary arithmetic), …
1
vote
Formulas for the liar paradox
Aladdin M. Yaqūb (1993) The Liar Speaks the Truth, OUP, formalises a very simple language for naturally expressing the liar paradox, consisting of:
First-order equational logic which may, but need n …
5
votes
Uses of bisimulation outside of computer science.
It's used in modal logic, where it was invented, and is used to define relations between models and constructions of new models from old models, which are used to show that different classes of model …
5
votes
What does it mean for a mathematical statement to be true?
Both the optimistic view that all true mathematical statements can be proven and its denial are respectable positions in the philosophy of mathematics, with the pessimistic view being more popular. T …
2
votes
What is the difference between the biconditional iff. and equality = ?
The worst problem with using equality in this way is that equality on propositions doesn't have a single meaning. Originally, in Boole's logic, it meant that one formula was obtained from another by …
8
votes
Accepted
Reducing ACA₀ proof to First Order PA
Chapter nine of Simpson (1999) Subsystems of Second-Order Arithmetic proves (a) by showing how to construct a second-order model for ACA0 from a first-order model of PA.
(b) The "second-order" we are …
4
votes
Can we prove set theory is consistent?
I think you are describing a process that is a fairly accurate description of how set theorists typically think about issues of consistency, where Set1 is the informal account of the cumulative hierar …
3
votes
Does the exact pair phenomenon for partial orders occur in your area of mathematics?
Rather than an answer, a comment that is too long to go where it belongs.
I'm guessing that this phenomenon is rarely observed, because mathematicians neither want to nor have much reason to deal wit …