Skip to main content
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
Search options not deleted user 22002

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 …
Mozibur Ullah's user avatar
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 …
Mozibur Ullah's user avatar
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 …
Mozibur Ullah's user avatar
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, …
Mozibur Ullah's user avatar
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 …
Mozibur Ullah's user avatar
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?
Mozibur Ullah's user avatar
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 …
Mozibur Ullah's user avatar
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 …
Mozibur Ullah's user avatar