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 1176
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
Question on Godel completeness theorem
I do not know from what angle you're coming, but "really exist" might mean "exists constructively". In this case you should look at Stefano Berardi, Silvio Valentini: Krivine's intuitionistic proof of …
- 48.8k
4
votes
Program transformation as alternative for Hoare logic or temporal logic
Hoare logic and temporal logic might be "the only known techniques for proving programs correct" to you, but there are certainly others!
For example, and this list is not exhaustive:
equational rea …
- 48.8k
13
votes
Accepted
Can ZFC prove "false theorems", and still be consistent? (was "Junk Theorems" follow up)
With the constraints you have imposed, the answer is negative. In practice, mathematicians write "normal mathematical statements" in a type theory which is then interpreted into ZFC. Because the inter …
- 48.8k
4
votes
Proof of second incompleteness theorem for Set theory without Arithmetization of Syntax
I understand the question to be about how to represent syntax internally in a theory. The traditional approach in logic is to use natural numbers and Gödel encodings.
Computer science, and in particul …
- 48.8k
8
votes
Accepted
Syntax/semantics conflation leads to infinitary logic
It sounds to me like this question is asking us to divine about the thinking of mathematicians in the early 20th century. Obviously, I can do no such thing, but perhaps I can explain how the early vie …
- 48.8k
14
votes
Second-order term in first-order logic?
While this question is not research-level, I think many mathematicians would not know how to answer it. I propose we keep it.
In usual logic texts first-order logic is done over a single sort, i.e., …
- 48.8k
4
votes
Ambiguity in ordered tuples
This has nothing to do with ordered tuples but rather with unions and disjoint unions.
You should use the disjoint union of all the $X^n$, not their union. Actually, to be quite precise, let $X$ be t …
- 48.8k
3
votes
Proof of Lindenbaum lemma without deduction theorem
You need classical logic for this. Presumably the following rules for negation are valid in your logic:
Elimination rule: if $\Delta \vdash \psi$ and $\Delta \vdash \neg\psi$ then $\Delta \vdash \bot …
- 48.8k
11
votes
Provable(P) ⇒ provable(provable(P))?
We work with Peano arithmetic PA. Following Goedel, in PA we can define a primitive recursive relation $\mathrm{Prf}(m,n)$ such that Peano arithmetic proves $\mathrm{Prf}(m,n)$ if, and only if, $n$ is …
- 48.8k
40
votes
A Model where Dedekind Reals and Cauchy Reals are Different
With classical logic or countable choice Cauchy and Dedekind reals coincide. Therefore we must look at a model of intuitionistic mathematics without countable choice, such as a topos of sheaves over a …
- 48.8k
9
votes
Accepted
A Proof that the Natural Numbers Form a pca?
For a formalization of Turing machines you could look at
Andrea Asperti and Wilmer Ricciotti: Formalizing Turing Machines. Lecture Notes in Computer Science Volume 7456, 2012, pp 1-25.
The book
…
- 48.8k
32
votes
Accepted
Impredicativity
Yes, it is worth the effort. A predicative version of an impredicative construction is typically more explicit and informative than the impredicative one. For example, consider the construction of a s …
- 48.8k
36
votes
What do we gain with higher order logics?
The debate about first-order and higher-order logics is a bit of a religious issue. There are many ways to argue one way or the other: first-order logic has very nice meta-theoretical properties, hig …
- 48.8k
17
votes
Accepted
What does "simplification of proofs as evaluation of programs" mean?
There are two inference rule of propositional logic involving implication (which I write using $\to$ instead of $\Rightarrow$):
The introduction rule says that we can prove $A \to B$ if we derive $B …
- 48.8k
4
votes
classical typed higher order logic natural deduction
Russell & Whiteheads theory is perhaps a bit on the heavy side, but here are some references to support Andreas Blass' comment:
An early formulations of classical higher-order logic was given by Alo …
- 48.8k