Elementary Syntax

02/02/2022

An inductive definition of even and odd numbers, from “Practical Foundations for Programming Languages” by Robert Harper (Section 2.5 for the curious). This defines the even and odd numbers with each other by declaring zero to be even and stating that if a number is odd, then it’s successor is even and if a number is even then it’s successor is odd.

01/31/2022

A variant of the Type Safety Theorem from "Practical Foundations for Programming Languages" by Robert Harper (Chapter 6 Theorem 6.1 for the curious). It states first that if e is of type t, and e evaluates to e', then e' must be of type t. Second if e is of type t then either e is a value of type t, or there exists some e' such that e evaluates to e'. These principles are called Preservation and Progress respectively. If for a simple programming language these requirements are fullfilled than the language is considered type safe.

01/28/2022

Wittgenstein never disappoints when it comes to unusual and deceptively profound ideas. Anyone know of any such works or care to undertake such a venture?

01/26/2022

The completeness of the Propositional Calculus, from Stephen Cole Kleene’s “Mathematical Logic” (Section 12, Theorem 14 for the curious). If a formula is valid, or tautological, then it is derivable in the classical propositional calculus using no assumptions other than the axioms and modus ponens.

01/24/2022

The consistency of the Propositional Calculus, from Stephen Cole Kleene’s “Mathematical Logic” (Section 11, Theorem 12 for the curious). If a formula E is derivable in the classical propositional calculus using no assumptions other than the axioms and modus ponens, then it is valid, or tautological.

01/21/2022

Kurt Gödel on the empirical sciences. One has to suspect he had some faith in the empirical sciences being a personal friend of Albert Einstein. What do you think he means by this? Comment your thoughts below!

01/19/2022

Introduction and Elimination rules for if/then from Stephen Cole Kleene’s “Mathematical Logic” (section 11 for the curious). A and B are formulas, G is some unspecified set of formulas, and ‘⊃’ signifies the if/then relationship. ‘⊢’ can be read as ‘yields’ and means that the following formulas are derivable from the preceding formulas.

01/17/2022

Duality rules for the propositional calculus from Stephen Cole Kleene’s “Mathematical Logic” (section 6 for the curious). E and F are formulas consisting only of atomic sentences and their negations, using only conjunction and disjunction for operations. E’ and F’ come from E and F simply by replacing all conjunctions with disjunctions, and all disjunctions with conjunctions. The
‘⊨’ can be read as ‘entails’ means the following formula is valid; it is true for all possible values of the atomic sentences composing it.

12/27/2021

An outline of my solution to Douglas R. Hofstadter's MU puzzle.

An overview of a solution to Douglas R Hofstadter's MU puzzle from the book "Gödel, Escher, Bach: an Eternal Golden Braid." What do you think of this solutio...

12/26/2021

I am a new course creator using the Thinkific platform aiming to bring difficult subjects into ordinary language, with a particular focus on logic, models, and theories.