This is an example of hybrid use of mechanized proofs with prose in a way that favors human readers.
It's a formalization and response to the central argument in The Futurlang vs. Natural Language Debate: Should Emotion Be Eradicated From Speech?. The argument was modeled using First-Order Logic in the Z3 prover.
Setup
There can be a thing.
A thing can be hindered.
A thing can be used.
There is a thing called precision, harmony, and progress.
There is a thing called natural language.
(declare-sort U)
(declare-fun optimize (U) Bool)
(declare-fun hinder (U) Bool)
(declare-fun we_use (U) Bool)
(declare-const precision_harmony_progress U)
(declare-const natural_language U)
P1: We optimize for precision, harmony, and progress.
(assert (optimize precision_harmony_progress))
P2: If we hinder a thing, we do not optimize for that thing.
(assert (forall ((x U))
(implies (hinder x) (not (optimize x)))))
P3: If we use natural language, we hinder precision, harmony, and progress.
(assert
(implies (we_use natural_language)
(hinder precision_harmony_progress)))
Therefore, we should not use natural language.
; Comments starting with "=>" indicate output.
(check-sat) ; => "sat"
(assert (we_use natural_language))
(check-sat) ; => "unsat"
I respond to this argument in two ways:
- Deny P1 because progress has not been sufficiently defined. Failure to define progress is a pitfall of Technological Postivism.
- Deny P3 because natural language does not strictly hinder harmony in the ways argued in the article. Specifically, emotional expression is neccessary for mutual understanding.
Let Language be Language and let Math be Math.