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 not deleted
user 2004
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.
8
votes
Accepted
Is any true sentence in the second-order Peano Axioms provable
Note that there are two different types of models of second-order logic: standard models, where second-order quantified variables range over all subsets of the domain; and Henkin models, where second- …
- 1,467
3
votes
Is there any proof assistant based on first-order logic?
You might want to search out John Harrison's book: Handbook of Practical Logic and Automated Reasoning. In the book he (among other things) develops an interactive theorem prover for first-order logic …
- 1,467
4
votes
Accepted
What restriction(s) of Goedel's primitive recursive functionals is (are) necessary and suffi...
Sorry for taking a bit longer to answer: Everything I say here is from Jeremy Avigad and Sol Feferman's article in the Handbook of Proof Theory, Gödel’s functional (“Dialectica”) interpretation: http: …
- 1,467
3
votes
Mechanically instantiating abstract constructions
I don't know if this answers your question, but here's how I would think about it. Work in a dependent type theory, and suppose we've defined a type of categories, $\mathrm{Cat}$. Suppose we've proved …
- 1,467
8
votes
Accepted
Reduction rules for inductive types
Your second reduction is called a commutative conversion. You can read about it in Girard, Taylor and Lafont, Proofs and Types, p. 80, for example. The congruence relation with commutative conversions …
- 1,467
2
votes
Why no morphisms from the contradictory proposition to the inconsistent context?
I'm not sure what you mean by the individual propositional objects having models or not.
In any case, as you said, as morphism in $\mathbb P$ simply is a context morphism compatible with the preorder …
- 1,467
7
votes
Accepted
Subcountability
An intuition for ESC (every set is subcountable, i.e., a subquotient of the natural numbers) in a predicative framework is that everything is built up from below starting with natural numbers, so we m …
- 1,467
6
votes
Accepted
A question about ordinal analysis
First of all, note that we don't (yet) have ordinal analyses of subsystems of second order arithmetic beyond $\Pi^1_2$-CA$_0$.
Still, we can say something about the pattern you indicate using known r …
- 1,467
7
votes
Accepted
Natural $\Pi^1_2$ (or worse) classes of structures?
An example that comes to mind is the set of recursive dilators; this is a $\Pi^1_2$-complete set (Theorem 4.1 in Girard 1985, Introduction to $\Pi^1_2$-logic). Dilators have some use outside of logic …
- 1,467
10
votes
Accepted
Arithmetic strength of Peano + the Howard ordinal
The answer is yes, using the ordinal analysis of KP. See Pohlers' A Short Course in Ordinal Analysis for why the usual ordinal analyses are profound, that is, they imply conservativity of the analyzed …
- 1,467
5
votes
Stronger theorem not resulting from proof analysis
Often we can easily prove something using impredicativity (e.g., by constructing something “from above” by taking the intersection of all solutions), while there may be a more difficult (or at least c …
5
votes
Can the Burgess-Hazen analysis of Predicative Arithmetic be extended to Transfinite Types?
I'm not aware of anyone doing the setup exactly as you describe, although it is very likely that it has been done, because it is very similar to Kreisel's proposed method of analyzing finitism in Ordi …
- 1,467
7
votes
Accepted
categorifying induction in homotopy type theory
The first reason you give is sufficient to answer your question: any interpretation of nat (and any other type with decidable equality) must have contractible components. Let me try to unpack the proo …
- 1,467
5
votes
Has the Ramified Theory of Types been applied to NBG?
You may be interested in Feferman's Unfolding Program, which gives a predicative closure to any schematic theory such as PA or ZFC. The unfolding of PA has the same strength as ATR$_0$, and Feferman c …
- 1,467