[FOM] Formalization Thesis

[Kaveh Ghasemloo]

Some short notes about Prof. Chow's FT, (many of them stated in
previous posts either implicitly or explicitly):

Aims of Formalization Thesis:
	1. Pragmatic: Every Mathematical Theorem Published in a Good Journal
is Formalizable in ZFC+"Some explicitly stated Axioms in the Paper"
	2. Philosophical: Mathematics is Formalizable (In reasonable (e.g.
recursive or constructive) theorie(s))

Versions:
	1. Local : Theory depends on Concept/Theorem
	2. Global : Theory is Fixed (Hilbert's Program)

Philosophical aim leads to discussing "What is *Mathematics*?" and
"What is a *Mathematical Concept/Result*?" "How does Mathematicians
Work/Will Work/Might Work/Have to Work?"
Pragmatical Aim leads to considering "How does a paper get published
in journals J1,...,Jn ?" (assuming no error occurs in this process)
Each of them might be justifiable in a way similar to Turing's
Analysis of a Human Computer.

It seems to me that mathematicians usually formalize a *Concept* in a
*Theory*, not just in a *Language*, since what you can prove about the
concept is important.

Formalization consists of two steps:
	Direct Formalization : Constructor, Decomposition, Possibly
Equivalence/Equality Relation, ... in general what we use to
work/define it, e.g.:
		Ordered Pair
			Constructor: x,y -> (x,y)
			Decompositions: p0(x,y)=x and p1(x,y)=y
			Equality : (x0,y0) = (x1,y1) iff x0=x1 and y0=y1

	Reduction : Interpretation in an Other Theory
		Ordered Pair in Set Theory
			Define (x,y) := {x,{x,y}}

Since we interpret a concept using an other one, it's natural to
expect that the interpretation will satisfy properties in the new
language that are not even expressible or meaningful in the original
one.

Types of Formalization:
	Faithful : No False Result is Provable
	Complete : All True Results are Provable

Formalization of (x,y) by {x,{x,y}} is faithful and complete

Of course one can argue, as Skolem did, that because of *compactness*
property of First Order Logic, many concepts like *finite*,
*well-oredered*, *complete (-ness of an ordered field)*, ... in an
intuitive sense are not faithfully  formalizable  in FOL at all.
-- 
Best
Kaveh Ghasemloo