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 answers only not deleted user 1176

Philosophical aspects of logic and set theory; truth status of mathematical axioms; Philosophy of Mathematics; philosophical aspects of mathematics in general; relation of mathematics to philosophy; etc. Consider also posting at http://philosophy.stackexchange.com/, where philosophy-of-mathematics is one of the most popular tags.

8 votes

What is an oracle, really?

The notion of "inner working" of an oracle is meaningless, because oracles are not machines. They are (infinite) input strings. In fact, it would be better to call oracles just input, as that would cr …
Andrej Bauer's user avatar
  • 48.8k
91 votes
Accepted

Is rigour just a ritual that most mathematicians wish to get rid of if they could?

I was not going to write anything, as I am a latecomer to this masterful troll question and not many are likely going to scroll all the way down, but Paul Taylor's call for Proof mining and Realizabil …
24 votes

Are the Foundations of Mathematical Logic Shaky?

No, they are not shaky. I answered a similar question before, but let me try again. You make a number of assumptions about logic. You are assuming that it is a goal of logic to bootstrap itself and …
Andrej Bauer's user avatar
  • 48.8k
7 votes

Sets = structured sets without structure

I find your approach somewhat puzzling. You seem to be saying that it useful to look at the property of "being a structure" rather than at the structure itself. What interesting mathematics do you int …
Andrej Bauer's user avatar
  • 48.8k
12 votes

Set-theoretical foundations of Mathematics with only bounded quantifiers

Most mathematics can be done in logical systems which are far weaker than Zermelo-Fraenkel set theory. For example, something like structural set theory will suffice for a great deal of ordinary mathe …
Andrej Bauer's user avatar
  • 48.8k
12 votes

Identity types: What makes Intuitionistic Type Theory *intuitionistic*?

As far as I can tell Martin-Löf's analysis of identity and his formulation of the identity types is the intuitionistic explanation of identity. In terms of BHK it would be an algorithmic version of Le …
Andrej Bauer's user avatar
  • 48.8k
15 votes
Accepted

synthetic differential geometry and other alternative theories

Perhaps I can make the implications of what Harry said a bit more explicit. A well-adapted model of SDG embeds smooths manifolds fully and faithfully. This in particualar means that the SDG model and …
Andrej Bauer's user avatar
  • 48.8k
13 votes

What types are to mathematical proofs as types à la Martin-Löf are to constructive proofs, a...

A good starting point to learn about type theories for classical logic is the $\lambda\mu$-calculus introduced in 1992 by Parigot in λμ-Calculus: An algorithmic interpretation of classical natural ded …
Andrej Bauer's user avatar
  • 48.8k
10 votes
Accepted

How to tell a paradox from a "paradox"?

Many paradoxes are first expressed in a semi-formal way, for example "the least number not describable by fewer than eleven words". They are warning signs that lead us to further analysis and can be r …
Andrej Bauer's user avatar
  • 48.8k
24 votes

Does the "propositions-as-types" paradigm match mathematical practice?

There are many aspects to the question "does a logical formalism reflect mathematical practice?" I will focus just on a very simple but important detail that every mathematician is familiar with. In …
Andrej Bauer's user avatar
  • 48.8k
9 votes

Categorification of logic

Honestly, I think your motivation is a bit misdirected, but apart from the answers already given, you should look at the general topic of categorical logic. Within that, there are category-theoretic t …
Andrej Bauer's user avatar
  • 48.8k
10 votes

Extensionality in HoTT versus extensionality in internal language of a category

The extension is the observable behavior, where "observation" means roughly "application of an eliminator". For a predicate $p$ we may observe whether it is true for a given argument, so by collecting …
Andrej Bauer's user avatar
  • 48.8k
13 votes

Are simplicial sets the intended model of HoTT?

My impression is as follows. While I cannot speak for Voevodsky, he certainly gives the impression that simplicial sets is his favorite, if not the intended model. For example, he would suggest axiom …
Andrej Bauer's user avatar
  • 48.8k
17 votes

Variable-centric logical foundation of calculus

I would like to argue in the opposite direction. The 17th century notation that is still in use today is a syntactic hodgepodge which does great disservice to students and their teachers alike, despit …
Andrej Bauer's user avatar
  • 48.8k
24 votes
Accepted

The Lucas argument vs the theorem-provers -- who wins and why?

Yes, computers can infer that the Gödel sentence is true. This is performed in a meta-theory which is stronger than the object theory, as it has to be. For example, Russell O'Connor formalized Gödel' …
Andrej Bauer's user avatar
  • 48.8k

15 30 50 per page