[FOM] 820: Sugared ZFC Formalization/2

[Lawrence Paulson]

There is a tension between logical formality and ordinary mathematical thinking. And because formality cannot be compromised (for then it would cease to be formal), ordinary mathematical thinking will need to give way. For example, ordinary mathematical thinking surely rejects both 1/0 = 1/0 and 1/0 ≠ 1/0 as meaningless. Most formal proof assistants will make the first one true and the second one false, though with free logic I believe it to be the other way around. There are other approaches to this particular difficulty, but doubt whether any of them are fully consistent with ordinary mathematical thinking. It is a vague concept so we can never be sure. We would be better off accepting a formal system whose workings can be understood with the help of ordinary mathematical thinking even when they are not strictly orthodox.

Larry Paulson



> On 14 Jun 2018, at 23:45, Harvey Friedman <hmflogic at gmail.com> wrote:
> 
> 2,3. THE BEST WAY TO PROCEED WITH ACTUAL
> FORMALIZATION IS TO START OVER WITH THE FUNDAMENTAL PRINCIPLE THAT
> ORDINARY MATHEMATICAL THINKING MUST RULE.