Mathematical foundations of Computer Science (CS) require great power as well as extreme rigor because of the requirement that computer systems be able to carry out all reasoning including reasoning about their own reasoning processes. The mathematical foundations of CS have important economic and security consequences.
Following a suggestion of [Scott 1967], mathematical foundations for Computer Science (CS) should be built on *both* types *and* sets:
* â€œthere is only one satisfactory way of avoiding the paradoxes: namely, the use of some form of the theory of types... the best way to regard Zermelo's theory is as a simplification and extension of Russell's ...simple theory of types. Now Russell made his types explicit in his notation and Zermelo left them implicit. It is a mistake to leave something so important invisible...â€
* â€œAs long as an idealistic manner of speaking about abstract objects is popular in mathematics, people will speak about collections of objects, and then collections of collections of ... of collections. In other words set theory is inevitable.â€ [emphasis in original]
A natural way to proceed is to construct sets from characteristic functions by composing function spaces on â„• (as axiomatised by Dedekind/Peano). Proceeding in this way, every set has finite rank. (The foundations of CS donâ€™t seem to need the higher cardinals.
However, theories of higher cardinals can be axiomatised in the foundations.) Sets in the foundations are categorical in the type Setsâ—…â„•â–», which is not a set (meaning that sets have been automatized up to isomorphism with a unique isomorphism). Categoricity is important for computer systems that reason model theoretically in order to avoid security holes. See â€œFormalizing common sense for scalable inconsistency-robust information integrationâ€ at Formalizing Common Sense.
Computer Science needs strong foundations that go far beyond the capabilities of first-order logic. For example, that a computer server provides service(i.e. âˆƒ[iâˆˆâ„•]â†’ ResponseBefore[i]) in the Actor Model) cannot be proved in a first-order theory.
Proof: In order to obtain a contradiction,suppose that it is possible to prove the theorem that computer server provides service (âˆƒ[iâˆˆâ„•]â†’ ResponseBefore[i]) in a first-order theory T. Therefore the following infinite set of sentences is inconsistent: {âŒˆÂ¬ResponseBefore[i]âŒ‰|iâˆˆâ„•}. By the compactness theorem of first-order logic, it follows that there is finite subset of the set of sentences that is inconsistent. But this is a contradiction, because all the finite subsets are consistent since the amount of time before a server responds is unbounded
âˆ„[iâˆˆâ„•]â†’ âŠ¢_{T} ResponseBefore[i]).
For further discussion, see â€œWhat is Computation? Actor Model versus Turingâ€™s Modelâ€.
Let Peano be the Peano/Dedekind theory of the natural numbers with the following strong induction axiom:
âˆ€[P:Boolean^{â„•}]â†’ Inductive[P]â‡¨âˆ€[iâˆˆâ„•]â†’ P[i]
where Inductive[P]â‡”P[0]âˆ§âˆ€[iâˆˆâ„•]â†’ P[i]â‡¨P[i+1]
Of course, there are inferentially undecidable propositions Î¨ such that
âŠ¬_{Peano}Î¨, âŠ¬_{Peano}Â¬Î¨, and âŠ¨_{â„•}Î¨. But this is not fundamental defect of the theory Peano (regardless that â„• is the categorical model of Peano) because in practice, proving âŠ¨_{â„•}Î¦ requires proving âŠ¢_{Peano} Î¦.
The exact nature of the inferentially undecidable propositions of Peano is currently a matter of great controversy. See â€œMathematics Self Proves its own Consistencyâ€.
Recent comments
1 week 5 days ago
1 week 6 days ago
1 week 6 days ago
2 weeks 20 hours ago
2 weeks 1 day ago
2 weeks 1 day ago
2 weeks 1 day ago
2 weeks 1 day ago
2 weeks 1 day ago
3 weeks 3 days ago