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 | |
Results tagged with lo.logic
Search options answers only
not deleted
user 1610
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.
65
votes
Accepted
Is there any formal foundation to ultrafinitism?
Wikipedia also says that Troelstra said in 1988 that there were no satisfactory foundations for ultrafinitism. Is this still true? Even if so, are there any aspects of ultrafinitism that you can get …
- 9,201
41
votes
Accepted
Presburger Arithmetic
Presburger arithmetic does NOT prove its own consistency. Its only function symbols are addition and successor, which are not sufficient to represent Godel encodings of propositions.
However, consiste …
- 9,201
33
votes
The unification of Mathematics via Topos Theory
This statement is true, but there's substantially less than meets the eye to it.
Topoi are gadgets which are both models of both a fairly large fragment of logic (typed higher-order logic), and are …
- 9,201
31
votes
Accepted
How do they verify a verifier of formalized proofs?
Is there such a "dumb" system around? If yes, do formalization projects use it? If not, do they recognize the need and put the effort into developing it? Or do they have other means to make their s …
- 9,201
31
votes
What is Realistic Mathematics?
At the other side, existence of large cardinals, non-measurable subsets of the reals, etc. are not (immediately) useful for such a study.
I don't know about non-measurable subsets, but large card …
- 9,201
23
votes
Accepted
How do proof verifiers work?
What exactly is the role of type theory in creating higher-order logics? Same goes with category theory/model theory, which I believe is an alternative.
Don't think of type theory, categori …
- 9,201
23
votes
Has decidability got something to do with primes?
Another evidence which I think might be relevant: The proof of the incompleteness theorems has some fancy part and some boring part. The fancy part involves Godel's Fixed point lemma and other thin …
- 9,201
22
votes
Community experiences writing Lamport's structured proofs
From a proof-theoretic point of view, Lamport essentially suggests is writing proofs in natural deduction style, along with a system of conventions to structure proofs by the relevant level of detail. …
21
votes
Proof assistants for mathematics
Honestly, part of the reason that proof assistants are focused on proving programs is precisely because of our very limited understanding of how to actually represent mathematics in formal logical sys …
21
votes
[solved] sequent calculus as programming language
There is no single answer to this question, because of the high degree of nondeterminism inherent in the sequent calculus -- to get a computational interpretation, you need to resolve the ambiguity, a …
- 9,201
21
votes
Are real numbers countable in constructive mathematics?
It depends on what you mean.
If you are working in classical mathematics, and regard the computable reals to be those real numbers for which a program exists to generate their digits, then they are …
- 9,201
20
votes
Proof strength of Calculus of (Inductive) Constructions
IIRC, the calculus of inductive constructions is equi-interpretable with ZFC plus countably many inaccessibles -- see Benjamin Werner's "Sets in Types, Types in Sets". (This is because of the presence …
- 9,201
18
votes
Can we disallow finite choice?
This is possible in constructive mathematics, because it distinguishes between finite sets and sets with a counted number of elements. (I'm not quite sure what the standard terminology is, though.)
A …
- 9,201
17
votes
Is there any relationship between Bourbaki's Epsilon Calculus and Lambda Calculus? Is $\lamb...
Bourbaki's tau-box notation is somewhat insane (e.g., see Adrian Mathias's A Term of Length 4,523,659,424,929), so I'll eventually answer in terms of Hilbert's epsilon-calculus.
But first, the laws o …
- 9,201
16
votes
Logic in mathematics and philosophy
I agree with Timothy and Andrej's answers, and will complement them by suggesting a few books by philosophers and philosophically-inclined logicians which I have found very interesting. I am sure the …
- 9,201