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.
3
votes
Inductive type constructors with the defined type appearing in non-strictly positive position
See the section Positivity, strict and otherwise of Counterexamples in Type Systems by Stephen Dolan. It explains the issues with non-strict positivity, it considers your example, and provides further …
- 48.8k
22
votes
Examples of mathematical theories that are naturally written in exotic logics
There is no end to "exotic logics" in computer science, and they express very natural things, such as behavior of programs, communication systems, security protocols, etc. To give just one example, Ho …
- 48.8k
7
votes
Mathematics without the principle of unique choice
I am not sure whether Yannick Forster is hanging out around here, so allow me to refer you to his PhD thesis and his recent research.
Yannick uses the following setup to carry out synthetic computabil …
- 48.8k
11
votes
Accepted
Does there exist a geometric morphism between the effective and topological topoi? Does one ...
There is no geometric morphism $f : E \to F$ if $E$ is a realizaiblity topos and $F$ is a Grothendieck topos. Indeed, if we had such an $f$, then for any indexing set $I$, the topos $E$ would have the …
- 48.8k
36
votes
Accepted
Is Bauer–Hanson’s result “there is a topos where the Dedekind reals are countable” novel?
[Update 2024-04-15: The preprint The countable reals is now available.]
Please allow me to list some basic observations that might clear up things. I work constructively (without excluded middle) and …
- 48.8k
8
votes
Hilbert's and Gödel's expanded definition of "Recursive Function"
In Recursive predicates and quantifiers (Trans. Amer. Math. Soc. 53 (1943), 41-73) Kleene gives a description of general recursive functions acording to Herbrand and Gödel, as understood before the pa …
- 48.8k
9
votes
Semantics of Higher-Order Logics
Here are some further possibilites:
Propositional logic: can be interpreted in any Boolean algebra (assuming you are talking about classical logic here), but perhaps your notion of truth assignment a …
- 1,446
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
18
votes
What's the earliest result (outside of logic) that cannot be proven constructively?
According to Wikipedia, in 5th century BCE, Bryson of Heraclea spoke of a special case of the intermediate value theorem. If we're very generous, that would be an early occurrence of a constructively …
- 48.8k
7
votes
Is univalence equivalent to every type function being a functor over equivalence?
Your axiom does not entail univalence.
It is consistent to add to type theory the isomorphism reflection rule
$$\frac{\Gamma \vdash e : A \simeq B}{\Gamma \vdash A \equiv B}$$
which states that equiva …
- 48.8k
4
votes
Is there one binary operation foundational for set theory?
There is a whole area of algebraic set theory. The internal language of a topos can be expressed as an essentially algebraic theory, see Lambek & Scott's "Introduction to higher-order categorical logi …
- 48.8k
10
votes
Accepted
How much choice is needed to prove the completeness of equational logic?
I do not know what proofs precisely you have in mind, but at least for operations with finite arities no choice is needed, nor excluded middle for that matter. Let us review the proof to make sure thi …
- 48.8k
6
votes
When can a function defined on $[a, b] \cup [b, c]$ be constructively extended to a function...
I am going to work Bishop-style (in particular I am giving myself countable choice, we can try to get rid of it later).
Observe that the Cauchy completion of $[a,b] \cup [b,c]$ is $[a,c]$. For this to …
- 48.8k
16
votes
Accepted
Church–Turing thesis for higher order functions
The answer to the question you ask can be found in John Longley's paper On the ubiquity of certain total type structures (PDF available here). Briefly, one can define the higher-type functionals by $N …
- 48.8k
11
votes
How exactly are realizability and the Curry-Howard correspondence related?
I am sure more than one exact correspondence can be made, but here's at least one that is technically precise. We shall employ categorical logic.
Executive summary: realizability is the interpretatio …
- 48.8k