Skip to main content
4 votes

Is there a multiway system which is equivalent to taking ZFC as axioms?

Wolfram's multi-way systems are expressive enough to accommodate generation of any computably enumerable set. Thus they are powerful enough to generate all theorems of a computably enumerable formal ...
Andrej Bauer's user avatar
  • 9,523
3 votes
Accepted

Negating universal/existential quantifier in type theory, propositions on elements of the empty type

The universal/existential quantifiers and their negations In type theory, negation is defined as a shortcut for "implying falsity", in other words ~ P is *...
Meven Lennon-Bertrand's user avatar
1 vote

Is there a multiway system which is equivalent to taking ZFC as axioms?

For a long time I have been interested in the idea of computationally enumerating every possible expression of a formal theory. Who hasn't! :) As one with a background in linguistics, I am sure you ...
Julio Di Egidio - inactive's user avatar

Only top scored, non community-wiki answers of a minimum length are eligible