Analyticity and Deduction
Overview
Formal definitions are given of the concepts analytic and demonstrative and it is proven that under these definitions the two concepts are coextensive. This is done twice using two slightly different models, the first very simple but with perhaps an unconvincing treatment of analyticity, the second a little more complex and hopefully a little more convincing.
The motivation for these models and the correspondence of the defined concepts with prior usage is discussed, and the models compared.
In this model the notion of analyticity in some language is effectively taken as primitive, by defining a semantics as an analyticity predicate. Language generic notions of analytic and demonstrative are then defined and shown to be coextensive.
An improved model of semantics is now adopted, permitting a more informative definition of analyticity and a stronger soundness predicate for the deductive systems, more closely matching usual practice in soundness proofs.
The treatment of the deductive system is refined by modelling a deductive system as an immediate derivability relation.
Introduction
The motivation for these models and the correspondence of the defined concepts with prior usage is discussed, and the models compared.
Motivation

For the purposes of an essay on the foundations of semantics I am seeking to motivate the study of semantic foundations with some words about the relationship between semantics and deduction. I thought a good way to do this would be to describe the concepts analytic and demonstrative and show that they are coextensive (given suitable but not unreasonable definitions).

I posted a first draft of this section to the yahoo group "philosophers group", which I had just joined expecting some discussion about the merits of the definitions, the significance of the result, or the details of the presentation, but not anticipating any debate about the truth of the conclusion, which is a trivial consequence of the definitions.

The truth of my "thesis" was disputed, and some pertinent questions were raised about the meaning of my definitions. I decided that formalisation would serve not only to make the meaning quite definite but also permit a (hopefully definitive) proof of the truth of my conclusion.

The first model which I produced was somewhat simpler than the original draft argument, particularly in its treatment of analyticity (the definition of which was one item on which clarification had been sought), so I produced a second slight elaboration in which the notion of analyticity is more fully treated and a better account of the notion of sound deductive system is given.

Remarks about Prior Usage
Analytic

As far as the fidelity of my formal definitions to prior usage is concerned, the concept of analyticity concerned here is intended to correspond closely to the concept as it was understood by the logical positivists, and also as it is described by Quine in his "Two Dogmas of Empiricism", which may be glossed as "true in virtue of meaning". I did have a bit of difficulty in expanding this "in virtue of" in the informal account, as necessary to permit the proof. This is not difficult in the formal models.

Demonstrative

The term demonstrative was chosen to connect in with the idea of formal derivability without ending up talking about all the possible conclusions of deductive proofs. Relevant precedents for this are the use of this term in Artistotle, Locke and Hume. An important feature of the term demonstrative is that a proof is only demonstrative if its premises are necessary (in Aristotle) or intuitive (in Locke and Hume) where it is clear in Locke and Hume that only necessary propositions can be intuitive in the required sense, and hence that, subject to suitable constraints on the soundness of the deductive system all demonstrative propositions are necessary.

Demonstrative (cont)

However, though the word "demonstrative" may be the best word, the primary desire was to connect the notion of analyticity with the kind of soundness proof which is conducted usually for a formal system to show (inter alia) its consistency. In this context the axioms are shown true with respect to the semantics, and the inference rules are shown to respect the semantics, with the effect that all the theorems are known to be true under the semantics, and hence analytic. It is the (rather elementary) connection between proof in sound deductive systems and the semantic notion of analyticity that is the target of the exercise, and therefore the defined concept of "demonstrative" is wholly semantic, does not talk about necessity, and might be thought to differ from the Aristotelian notion on that account.

A further difficulty arised from incompleteness. There is no single (r.e.) deductive system which proves all the analytic truths. In these models, the only constraint on axioms is that they are analytic, and the only constraint on inference rules is that they preserve truth under the relevant semantics. This does yeild the desired identity, but certainly represents a more liberal deductive regime than that in Locke and Hume, who require that the axioms and rules be intuitively certain. To get the identity I am in effect permitting sound deductive systems in which the most tenuous and obscure (but true) large cardinal axioms are employed, and it is doubtful that Locke would have thought these intuitively certain.

So far as Aristotle is concerned, the rules are syllogistic, and he has no conception of the linguistically pluralistic world inhabited by modern logicians, so again our notion of demonstrative is on the generous side.

Model 1
In this model the notion of analyticity in some language is effectively taken as primitive, by defining a semantics as an analyticity predicate. Language generic notions of analytic and demonstrative are then defined and shown to be coextensive.
The Theory x003t
The new theory is first created.
xl-sml
open_theory "hol";
force_new_theory "x003t";
set_pc "hol";

Language and Semantics

A language is a set of sentences with a given semantics. For present purpose a truth conditional semantics is sufficient. In fact all we need to know is what sentences in the language are analytic (which is a subset of the information we would normally expect to be derivable from the truth conditions), so we model "a semantics" as a predicate over the sentences of a language which tells you which of them are analytic. A language may be thought of as two properties of sentences, the property of being well formed and the property of being analytic, but in fact we do not make use of this concept and therefore do not provide a definition.

Analytic

We here define analtyic as a property of ordered pairs of which the first is a sentence and the second is a semantics for the some language. Since a semantics in this model is just an analyticity predicate, sentence sen is analytic under the semantics sem iff the predicate sem is true of the sentence sen. The application of a predicate is function application, which is written by juxtapostion so this is written simply as sem sen.


xl-holconst
fttabanalytic : 's × ('s → BOOL) → BOOL
fttab∀sen sem• analytic (sen, sem) ≡ sem sen
Sound Deductive System

A deductive system is a relation between sets of sentences and sentences, that of derivability. Soundness is a relation between deductive systems and semantics, that of preserving analyticity. i.e. a deductive system is sound if whenever all of the premises of an inference are analytic so is the conclusion. This is a weaker condition than is normally proved in a soundness proof, but it suffices for our purposes, and cannot be strengthened without a more informative model of the semantics.


xl-holconst
fttabsound : (('s → BOOL) × 's → BOOL) × ('s → BOOL) → BOOL
fttab∀ds sem• sound (ds, sem)
fttab≡ ∀prem conc• ds (prem, conc)
fttab ⇒ ((∀s• prem s ⇒ sem s) ⇒ sem conc)
Demonstrative

demonstrative is a relation between sentences and semantics (that the sentence is derivable in a deductive system which is sound with respect to that semantics). A sentence is demonstrative under a semantics if there is a deductive system, sound with respect to that semantics, under which the sentence is derivable from the empty set of premises. The "empty set of premises" is modelled as an always false (contradictory) predicate, which is written as the lambda abstraction ⌜λs•F⌝, the function which always returns "false".


xl-holconst
fttabdemonstrative : 's × ('s → BOOL) → BOOL
fttab∀sen sem• demonstrative (sen, sem)
fttab≡ ∃ ds• sound (ds, sem) ∧ ds ((λs•F), sen)
The Proof
The following is the proof that analytic and demonstrative are coextensive.
xl-sml
set_goal([], ⌜∀sen sem• analytic (sen, sem) ≡ demonstrative (sen, sem)⌝);
a (rewrite_tac(map get_spec [
fttabfttab⌜analytic⌝,
fttabfttab⌜demonstrative⌝,
fttabfttab⌜sound⌝]));


xl-gft
(* ?⊢ *) ⌜∀ sen sem
ftbr • sem sen
ftbr ≡ (∃ ds
ftbr • (∀ prem conc• ds (prem, conc) ⇒ (∀ s• prem s ⇒ sem s) ⇒ sem conc)
ftbr ∧ ds ((λ s• F), sen))⌝


xl-sml
a (REPEAT strip_tac);


xl-gft
(* *** Goal "2" *** *)

(* 2 *) ⌜∀ prem conc• ds (prem, conc) ⇒ (∀ s• prem s ⇒ sem s) ⇒ sem conc⌝
(* 1 *) ⌜ds ((λ s• F), sen)⌝

(* ?⊢ *) ⌜sem sen⌝


(* *** Goal "1" *** *)

(* 1 *) ⌜sem sen⌝

(* ?⊢ *) ⌜∃ ds
ftbr • (∀ prem conc• ds (prem, conc) ⇒ (∀ s• prem s ⇒ sem s) ⇒ sem conc)
ftbr ∧ ds ((λ s• F), sen)⌝


xl-sml
(* *** Goal "1" *** *)
a (∃_tac ⌜λ(ss,s)• s = sen⌝
fttabTHEN rewrite_tac[]);


xl-gft
(* 1 *) ⌜sem sen⌝

(* ?⊢ *) ⌜∀ prem conc• conc = sen ⇒ (∀ s• prem s ⇒ sem s) ⇒ sem conc⌝


xl-sml
a (REPEAT strip_tac
fttabTHEN asm_rewrite_tac[]);


xl-gft
Current goal achieved, next goal is:

(* *** Goal "2" *** *)

(* 2 *) ⌜∀ prem conc• ds (prem, conc) ⇒ (∀ s• prem s ⇒ sem s) ⇒ sem conc⌝
(* 1 *) ⌜ds ((λ s• F), sen)⌝

(* ?⊢ *) ⌜sem sen⌝


xl-sml
(* *** Goal "2" *** *)
a (list_spec_nth_asm_tac 2 [⌜(λ s• F)⌝, ⌜sen⌝]);


xl-gft
(* 4 *) ⌜∀ prem conc• ds (prem, conc) ⇒ (∀ s• prem s ⇒ sem s) ⇒ sem conc⌝
(* 3 *) ⌜ds ((λ s• F), sen)⌝
(* 2 *) ⌜(λ s• F) s⌝
(* 1 *) ⌜¬ sem s⌝

(* ?⊢ *) ⌜sem sen⌝


xl-sml
a (swap_nth_asm_concl_tac 2
fttabTHEN rewrite_tac[]);


xl-gft
Current and main goal achieved


xl-sml
save_pop_thm "Theorem1";

Model 2
An improved model of semantics is now adopted, permitting a more informative definition of analyticity and a stronger soundness predicate for the deductive systems, more closely matching usual practice in soundness proofs.
The Theory x003u
The new theory is first created.
xl-sml
open_theory "hol";
force_new_theory "x003u";
set_pc "hol";

Language and Semantics

We now model a semantics as a full account of truth conditions. For this we use a function which tells you under what circumstances a sentence is true. What a "circumstance" is depends upon the language, but for a language talking about the world it would typically be something like a possible world plus an assignment to free variables of values in that possible world.

As far as this model is concerned the structure of a circumstance is immaterial and the type variable qqco.gif'c⌝ is used. A semantics, for the purposes of this model is therefore something of type qqco.gif's → 'c → BOOL⌝. This is a higher order function which takes two arguments, first a sentence then a "circumstance", and yields the truth value of the sentence under those circumstances. In other words, a semantics is a function which assigns to each sentence of the language the set of conditions under which it is true.

This change has only very minor consequences for the model and the proof. It does permits a more informative definition of analyticity and a more realistic account of what it is for a deductive system to be sound. One extra step is needed in the proof script.

Note that the use of the term sentence here differs from the usage specific to the first order predicate calculus in that a sentence is not required to be closed.

Analytic

The definition of analytic says that a sentence is analytic if it is true under the semantics whatever the "circumstances". i.e. you can tell that its true from the semantics alone, without knowing the "facts" (the second argument to the truth valuation function). sem sen c is the truth value of sentence sen in circumstances c under semantics sem.


xl-holconst
fttabanalytic : 's × ('s → 'c → BOOL) → BOOL
fttab∀sen sem• analytic (sen, sem) ≡ ∀c• sem sen c
Sound Deductive System

Instead of saying that a sound deductive system is one which preserves analyticity, we now say that it preserves truth under all circumstances. i.e. if ⌜(prem, conc)⌝ is a derivation under the deductive system, then under every circumstance which satisfies all sentences in the premises ⌜prem⌝ will also satisfy the conclusion ⌜conc⌝ (all this relative to some specific semantics).


xl-holconst
fttabsound : (('s → BOOL) × 's → BOOL)
fttabfttab× ('s → 'c → BOOL)
fttabfttab→ BOOL
fttab∀ds sem• sound (ds, sem)
fttab≡ ∀prem conc• ds (prem, conc)
fttab ⇒ ∀c• ((∀s• prem s ⇒ sem s c) ⇒ sem conc c)
Demonstrative

demonstrative is a relation between sentences and semantics (that the sentence is derivable in a deductive system which is sound with respect to that semantics). This definition is unchanged from the first model, though it now uses the revised soundness predicate and consequently has a different type.


xl-holconst
fttabdemonstrative : 's × ('s → 'c → BOOL) → BOOL
fttab∀sen sem• demonstrative (sen, sem)
fttab≡ ∃ ds• sound (ds, sem) ∧ ds ((λs•F), sen)
The Proof
The following is the proof that analytic and demonstrative are coextensive.
xl-sml
set_goal([], ⌜∀sen sem• analytic (sen, sem) ≡ demonstrative (sen, sem)⌝);
a (rewrite_tac(map get_spec [
fttabfttab⌜analytic⌝,
fttabfttab⌜demonstrative⌝,
fttabfttab⌜sound⌝]));


xl-gft
(* ?⊢ *) ⌜∀ sen sem
ftbr • (∀ c• sem sen c)
ftbr ≡ (∃ ds
ftbr • (∀ prem conc• ds (prem, conc) ⇒ (∀ c• (∀ s• prem s ⇒ sem s c) ⇒ sem conc c))
ftbr ∧ ds ((λ s• F), sen))⌝


xl-sml
a (REPEAT strip_tac);


xl-gft
(* *** Goal "2" *** *)

(* 2 *) ⌜∀ prem conc• ds (prem, conc) ⇒ (∀ c• (∀ s• prem s ⇒ sem s c) ⇒ sem conc c)⌝
(* 1 *) ⌜ds ((λ s• F), sen)⌝

(* ?⊢ *) ⌜sem sen c⌝

(* *** Goal "1" *** *)

(* 1 *) ⌜∀ c• sem sen c⌝

(* ?⊢ *) ⌜∃ ds
ftbr • (∀ prem conc• ds (prem, conc) ⇒ (∀ c• (∀ s• prem s ⇒ sem s c) ⇒ sem conc c))
ftbr ∧ ds ((λ s• F), sen)⌝


xl-sml
a (∃_tac ⌜λ(ss, s)• s = sen⌝ THEN rewrite_tac[]);


xl-gft
(* 1 *) ⌜∀ c• sem sen c⌝

(* ?⊢ *) ⌜∀ prem conc• conc = sen ⇒ (∀ c• (∀ s• prem s ⇒ sem s c) ⇒ sem conc c)⌝


xl-sml
a (REPEAT strip_tac THEN asm_rewrite_tac[]);


xl-gft
Current goal achieved, next goal is:

(* *** Goal "2" *** *)

(* 2 *) ⌜∀ prem conc• ds (prem, conc) ⇒ (∀ c• (∀ s• prem s ⇒ sem s c) ⇒ sem conc c)⌝
(* 1 *) ⌜ds ((λ s• F), sen)⌝

(* ?⊢ *) ⌜sem sen c⌝


xl-sml
a (list_spec_nth_asm_tac 2 [⌜(λ s• F)⌝, ⌜sen⌝]);


xl-gft
(* 3 *) ⌜∀ prem conc• ds (prem, conc) ⇒ (∀ c• (∀ s• prem s ⇒ sem s c) ⇒ sem conc c)⌝
(* 2 *) ⌜ds ((λ s• F), sen)⌝
(* 1 *) ⌜∀ c• (∀ s• (λ s• F) s ⇒ sem s c) ⇒ sem sen c⌝

(* ?⊢ *) ⌜sem sen c⌝


xl-sml
a (spec_nth_asm_tac 1 ⌜c⌝);


xl-gft
(* 5 *) ⌜∀ prem conc• ds (prem, conc) ⇒ (∀ c• (∀ s• prem s ⇒ sem s c) ⇒ sem conc c)⌝
(* 4 *) ⌜ds ((λ s• F), sen)⌝
(* 3 *) ⌜∀ c• (∀ s• (λ s• F) s ⇒ sem s c) ⇒ sem sen c⌝
(* 2 *) ⌜(λ s• F) s⌝
(* 1 *) ⌜¬ sem s c⌝

(* ?⊢ *) ⌜sem sen c⌝


xl-sml
a (all_asm_ante_tac THEN rewrite_tac[]);


xl-gft
Current and main goal achieved


xl-sml
save_pop_thm "Theorem1";

Model 3
The treatment of the deductive system is refined by modelling a deductive system as an immediate derivability relation.
The Theory x003v
The new theory is first created.
xl-sml
open_theory "hol";
force_new_theory "x003v";
set_pc "hol";

Language and Semantics

This is unchanged from model 2.

Analytic

Unchanged.


xl-holconst
fttabanalytic : 's × ('s → 'c → BOOL) → BOOL
fttab∀sen sem• analytic (sen, sem) ≡ ∀c• sem sen c
Sound Deductive System

The definition of soundness remains formally unchanged, but the deductive system is now to be understood as an immediate derivability relation.


xl-holconst
fttabsound : (('s → BOOL) × 's → BOOL)
fttabfttab× ('s → 'c → BOOL)
fttabfttab→ BOOL
fttab∀ds sem•
fttab sound (ds, sem) ≡
fttabfttab∀prem conc•
fttabfttabfttabds (prem, conc)
fttab fttabfttab⇒ ∀c• ((∀s• prem s ⇒ sem s c) ⇒ sem conc c)
Derivation

We now define a function which lifts an immediate derivability relation to a derivability relation.

The following defines the property of properties of sets of sentences of being closed under an immediate inference relation.


xl-holconst
fttabiiclosed : (('s → BOOL) × 's → BOOL)
fttabfttab→ ('s → BOOL) → BOOL
fttab∀ds ss•
fttab iiclosed ds ss ≡
fttabfttab∀prems conc•
fttabfttabfttabds (prems, conc) ∧ (∀s• prems s ⇒ ss s)
fttabfttabfttab⇒ ss conc

The closure of a relation of immediate inference is now defined, i.e. the corresponding notion of derived inference.


xl-holconst
fttabclose_ds : (('s → BOOL) × 's → BOOL)
fttabfttab→ (('s → BOOL) × 's → BOOL)
fttab∀ds prems conc•
fttab close_ds ds (prems, conc) ≡
fttab fttab∀css• iiclosed ds css ∧ (∀t• prems t ⇒ css t) ⇒ css conc
Demonstrative

demonstrative is a relation between sentences and semantics (that a sentence is derivable in a deductive system which is sound with respect to that semantics). The definition now reflects that a deductive system is represented by an immediate inference relation, and that sentences are provable if they are reachable by the corresponding derived inference relation.


xl-holconst
fttabdemonstrative : 's × ('s → 'c → BOOL) → BOOL
fttab∀sen sem•
fttab demonstrative (sen, sem) ≡
fttabfttab∃ ds• sound (ds, sem) ∧ (close_ds ds) ((λs•F), sen)
The Proof

The proof now must effectively incorporate the demonstration that if an immediate inference relation is sound then so is the derived inference relation obtained from it.

First I proved a lemma stating that the derived inference rules are sound iff the immediate inference rules are sound, viz:
xl-sml
set_goal([], ⌜∀ds• sound (ds, sem) ≡ sound (close_ds ds, sem)⌝);

But then I didn't use it in the main proof so the proof of the lemma is not listed. The following is the proof that analytic and demonstrative are coextensive.
xl-sml
set_goal([], ⌜∀sen sem• analytic (sen, sem) ≡ demonstrative (sen, sem)⌝);
a (rewrite_tac(map get_spec [
fttabfttab⌜analytic⌝,
fttabfttab⌜demonstrative⌝,
fttabfttab⌜sound⌝])
fttabTHEN REPEAT strip_tac);


xl-gft
(* *** Goal "2" *** *)

(* 2 *) ⌜∀ prem conc• ds (prem, conc) ⇒ (∀ c• (∀ s• prem s ⇒ sem s c) ⇒ sem conc c)⌝
(* 1 *) ⌜close_ds ds ((λ s• F), sen)⌝

(* ?⊢ *) ⌜sem sen c⌝

(* *** Goal "1" *** *)

(* 1 *) ⌜∀ c• sem sen c⌝

(* ?⊢ *) ⌜∃ ds
ftbr • (∀ prem conc• ds (prem, conc) ⇒ (∀ c• (∀ s• prem s ⇒ sem s c) ⇒ sem conc c))
ftbr ∧ close_ds ds ((λ s• F), sen)⌝


xl-sml
(* *** Goal "1" *** *)
a (∃_tac ⌜λ(ss, s)• s = sen⌝
fttabTHEN rewrite_tac[]
fttabTHEN REPEAT strip_tac
fttabTHEN_TRY asm_rewrite_tac[]);


xl-gft
(* 1 *) ⌜∀ c• sem sen c⌝

(* ?⊢ *) ⌜close_ds (λ (ss, s)• s = sen) ((λ s• F), sen)⌝


xl-sml
a (asm_rewrite_tac[get_spec ⌜close_ds⌝,
fttabget_spec ⌜iiclosed⌝]
fttabTHEN REPEAT strip_tac);


xl-gft
(* 2 *) ⌜∀ c• sem sen c⌝
(* 1 *) ⌜∀ prems conc• conc = sen ∧ (∀ s• prems s ⇒ css s) ⇒ css conc⌝


xl-sml
a (LIST_SPEC_NTH_ASM_T 1 [⌜(λ s• F)⌝, ⌜sen⌝] ante_tac
fttabTHEN rewrite_tac[]);


xl-gft
Current goal achieved, next goal is:

(* *** Goal "2" *** *)

(* 2 *) ⌜∀ prem conc• ds (prem, conc) ⇒ (∀ c• (∀ s• prem s ⇒ sem s c) ⇒ sem conc c)⌝
(* 1 *) ⌜close_ds ds ((λ s• F), sen)⌝

(* ?⊢ *) ⌜sem sen c⌝


xl-sml
a (POP_ASM_T ante_tac
fttabTHEN rewrite_tac [
fttabfttabget_spec ⌜close_ds⌝,
fttabfttabget_spec ⌜iiclosed⌝]
fttabTHEN REPEAT strip_tac);


xl-gft
(* 2 *) ⌜∀ prem conc• ds (prem, conc) ⇒ (∀ c• (∀ s• prem s ⇒ sem s c) ⇒ sem conc c)⌝
(* 1 *) ⌜∀ css
ftbr • (∀ prems conc• ds (prems, conc) ∧ (∀ s• prems s ⇒ css s) ⇒ css conc) ⇒ css sen⌝

(* ?⊢ *) ⌜sem sen c⌝


xl-sml
a (SPEC_NTH_ASM_T 1 ⌜λ s• sem s c⌝ ante_tac
fttabTHEN rewrite_tac[]
fttabTHEN REPEAT strip_tac
fttabTHEN all_asm_fc_tac[]);


xl-gft
Tactic produced 0 subgoals:
Current and main goal achieved


xl-sml
val Theorem1 = save_pop_thm "Theorem1";


up quick index © RBJ

privacy policy

Created:

$Id: x003.xml,v 1.6 2008/04/06 13:07:17 rbj01 Exp $

V