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.
2
votes
0
answers
107
views
Is there a nice theorem that makes essential use of types in typed first-order logic?
I've read (somewhere) that types in typed first-order logic is just 'syntactic sugar'.
But, surely there is more to than that?
For example: the upper-bound property of the reals can't be expressed i …
3
votes
0
answers
241
views
is there any connection between the consistent histories interpretation of quantum mechanics...
Kripke semantics interpret intuitionistic logic by a partially ordered set of worlds/situations. Consistent histories interpretation of QM elaborates the copenhagen interpretation where a consistent s …
5
votes
2
answers
654
views
What is the analogue for the category of presheafs for complement toposes?
Complement Toposes are dual in a sense to (elementary) Toposes and are expected to have typed higher paraconsistent logic as its internal language (as dual intuitionistic logic is paraconsistent).
No …
3
votes
0
answers
199
views
Is there a useful Galois connection between Languages and Grammars?
I've just beginning to learn logic and proof theory - and the following rather vague and perhaps ill-formed question occurred to me.
Given an alphabet it's straightforward to construct the Language, …
4
votes
2
answers
744
views
What is the impact on Godels theorem of Paraconsistency?
Russells paradox forced a restriction of the natural abstraction principle (that every predicate determines a set) so that Set Theory could be consistent. The standard one being ZF.
However paraconsi …
6
votes
2
answers
603
views
What categories correspond to the typed lambda calculus with parametric types?
the unadorned typed lambda calculus correspond to the closed cartesian categories, but if we add in dependent or parametric types how are they then characterised?
9
votes
1
answer
709
views
Is there a nice characterisation of topoi with nice meta-logical properties?
First-order order classical logic with standard semantics has a proof theory: it is complete, sound and effective.
In higher order logic with standard semantics one cannot obtain a proof theory - i …
0
votes
Essential reads in the philosophy of mathematics and set theory
Borges 'The Library of Babel' is a beautiful meditation on all sorts of philosophical positions around the 'idea' of infinity, epistemology, the sociology of science, set theory paradoxes. Its literat …
20
votes
4
answers
4k
views
Is there a categorical proof of Gödel's incompleteness theorem?
A significant result in set theory was shown by Cohen when he showed that the continuum hypothesis was independent of ZFC using a new technique called forcing. In Topos theory, this result has a new g …