
11The failsafe makes sure the fee is high enough to meet carbon emission reduction targets. The safeguard keeps the fee from getting any higher than needed. One of the ways that we could account for the unpredictability of the price elasticity of demand for carbon would be to provide a failsafe mechanism to ensure that we definitely stay on the carbon reduction schedule. If we keep Energy Innovation Act (HR 763) essentially as it is and scale up the annual carbon fee increase by NumberofYears…Read more

14One of the ways that we could account for the unpredictability of the price elasticity of demand for carbon would be to provide a failsafe mechanism to ensure that we definitely stay on the carbon reduction schedule. If we kept Energy Innovation Act (HR 763) essentially as it is and scale up the annual carbon fee increase by NumberofYearsBehindSchedule * 0.15.

22When we look at 800,000 year ice core data CO2 levels since 1950 have risen at a rate of 123fold faster than the fastest rate in 800,000 years. When we see that this rise is precisely correlated with global carbon emissions the human link to climate change seems certain and any rebuttal becomes ridiculously implausible. The 800,000 year correlation between CO2 and global temperatures seems to be predicting at least 9 degrees C of more warming based on current CO2 levels.

94When we sum up the results of Gödel's 1931 Incompleteness Theorem by formalizing Wittgenstein’s verbal specification such that this formalization meets Gödel's own sufficiency requirement: ”Every epistemological antinomy can likewise be used for a similar undecidability proof." then we can see that Gödel's famous logic sentence is only unprovable in PA because it is untrue in PA because it specifies the logical equivalence to self contradiction in PA.

64Could the intersection of [formal proofs of mathematical logic] and [sound deductive inference] specify formal systems having [deductively sound formal proofs of mathematical logic]? All that we have to do to provide [deductively sound formal proofs of mathematical logic] is select the subset of conventional [formal proofs of mathematical logic] having true premises and now we have [deductively sound formal proofs of mathematical logic].

27Both Tarski and Gödel “prove” that provability can diverge from Truth. When we boil their claim down to its simplest possible essence it is really claiming that valid inference from true premises might not always derive a true consequence. This is obviously impossible.

58To eliminate incompleteness, undecidability and inconsistency from formal systems we only need to convert the formal proofs to theorem consequences of symbolic logic to conform to the sound deductive inference model. Within the sound deductive inference model there is a (connected sequence of valid deductions from true premises to a true conclusion) thus unlike the formal proofs of symbolic logic provability cannot diverge from truth.

58Tarski "proved" that there cannot possibly be any correct formalization of the notion of truth entirely on the basis of an insufficiently expressive formal system that was incapable of recognizing and rejecting semantically incorrect expressions of language. The only thing required to eliminate incompleteness, undecidability and inconsistency from formal systems is transforming the formal proofs of symbolic logic to use the sound deductive inference model.

32The generalized conclusion of the Tarski and Gödel proofs: All formal systems of greater expressive power than arithmetic necessarily have undecidable sentences. Is not the immutable truth that Tarski made it out to be it is only based on his starting assumptions. When we reexamine these starting assumptions from the perspective of the philosophy of logic we find that there are alternative ways that formal systems can be defined that make undecidability inexpressible in all of these formal syste…Read more

50If the conclusion of the Tarski Undefinability Theorem was that some artificially constrained limited notions of a formal system necessarily have undecidable sentences, then Tarski made no mistake within his assumptions. When we expand the scope of his investigation to other notions of formal systems we reach an entirely different conclusion showing that Tarski's assumptions were wrong.

301Because formal systems of symbolic logic inherently express and represent the deductive inference model formal proofs to theorem consequences can be understood to represent sound deductive inference to true conclusions without any need for other representations such as model theory.

45Because formal systems of symbolic logic inherently express and represent the deductive inference model formal proofs to theorem consequences can be understood to represent sound deductive inference to deductive conclusions without any need for other representations.

52This is the formal YACC BNF specification for Minimal Type Theory (MTT). MTT was created by augmenting the syntax of First Order Logic (FOL) to specify Higher Order Logic (HOL) expressions using FOL syntax. Syntax is provided to enable quantifiers to specify type. FOL is a subset of MTT. The ASSIGN_ALIAS operator := enables FOL expressions to be chained together to form HOL expressions.

4In this paper we show how to define a halting decidability decider that rejects all finite string Turing machine descriptions that would otherwise make halting undecidable. All of the conventional halting problem proof counterexamples would be rejected on the basis that they specify an infinitely recursive evaluation sequence thus are malformed expressions of the language of Turing Machine descriptions.

127For any natural (human) or formal (mathematical) language L we know that an expression X of language L is true if and only if there are expressions Γ of language L that connect X to known facts. By extending the notion of a Well Formed Formula to include syntactically formalized rules for rejecting semantically incorrect expressions we recognize and reject expressions that evaluate to neither True nor False.

157If there truly is a proof that shows that no universal halt decider exists on the basis that certain tuples: (H, Wm, W) are undecidable, then this very same proof (implemented as a Turing machine) could be used by H to reject some of its inputs. Whensoever the hypothetical halt decider cannot derive a formal proof from its input strings and initial state to final states corresponding the mathematical logic functions of Halts(Wm, W) or Loops(Wm, W), halting undecidability has been decided.

69When we understand that every potential halt decider must derive a formal mathematical proof from its inputs to its final states previously undiscovered semantic details emerge. Whensoever the potential halt decider cannot derive a formal proof from its input strings to its final states of Halts or Loops, undecidability has been decided. The formal proof involves tracing the sequence of state transitions of the input TMD as syntactic logical consequence inference steps in the formal languag…Read more

29By extending the notion of a Well Formed Formula to include syntactically formalized rules for rejecting semantically incorrect expressions we recognize and reject expressions that have the semantic error of Pathological selfreference(Olcott 2004). The foundation of this system requires the notion of a BaseFact that anchors the semantic notions of True and False. Whensoever a formal proof from BaseFacts of language L to a closed WFF X or ~X of language L does not exist X is decided to be sema…Read more

125Minimal Type Theory (MTT) shows exactly how all of the constituent parts of an expression relate to each other (in 2D space) when this expression is formalized using a directed acyclic graph (DAG). This provides substantially greater expressiveness than the 1D space of FOPL syntax. The increase in expressiveness over other formal systems of logic shows the Pathological SelfReference Error of expressions previously considered to be sentences of formal systems. MTT shows that these expressions …Read more

398This paper decomposes the Liar Paradox into its semantic atoms using Meaning Postulates (1952) provided by Rudolf Carnap. Formalizing truth values of propositions as Boolean properties of these propositions is a key new insight. This new insight divides the translation of a declarative sentence into its equivalent mathematical proposition into three separate steps. When each of these steps are separately examined the logical error of the Liar Paradox is unequivocally shown.

238Hypothesis: WFF(x) can be applied syntactically to the semantics of formalized declarative sentences such that: WFF(x) ↔ (x ↦ True) ∨ (x ↦ False) (see proof sketch below) For clarity we focus on simple propositions without binary logical connectives.

266Within the (Haskell Curry) notion of a formal system we complete Tarski's formal correctness: ∀x True(x) ↔ ⊢ x and use this finally formalized notion of Truth to refute his own Undefinability Theorem (based on the Liar Paradox), the Liar Paradox, and the (Panu Raatikainen) essence of the conclusion of the 1931 Incompleteness Theorem.

73We begin with the hypothetical assumption that Tarski’s 1933 formula ∀ True(x) φ(x) has been defined such that ∀x Tarski:True(x) ↔ BooleanTrue. On the basis of this logical premise we formalize the Truth Teller Paradox: "This sentence is true." showing syntactically how selfreference paradox is semantically ungrounded.

480Minimal Type Theory (MTT) is based on type theory in that it is agnostic about Predicate Logic level and expressly disallows the evaluation of incompatible types. It is called Minimal because it has the fewest possible number of fundamental types, and has all of its syntax expressed entirely as the connections in a directed acyclic graph.
Areas of Specialization
Epistemology 
Philosophy of Language 
Logic and Philosophy of Logic 
Areas of Interest
Epistemology 
Philosophy of Language 
Logic and Philosophy of Logic 