Stream: Coq users

Topic: No True Scotsman fallacy formalization.

Thomas Dziedzic (Aug 14 2023 at 13:03):

Hey all, I was trying to write a Theorem (not even proof) for the No True Scotsman fallacy, and I seem to be stuck. https://en.wikipedia.org/wiki/No_true_Scotsman

The closest working solution I came up with was:

``````Theorem counter_example_negates_generalization :
forall
{A : Type} {P : Prop}
{eq_dec : forall x y : A, {x = y}+{x <> y}}
(scotsmen : list A)
(generalization : forall scotsman, In scotsman scotsmen -> P)
(counter_example : exists counter_scotsman, In counter_scotsman scotsmen /\ ~P),
False.
Proof.
intros.
destruct counter_example as [counter_scotsman [counter_example_IN counter_example_NP]].
apply counter_example_NP.
apply (generalization counter_scotsman).
assumption.
Qed.
``````

But I can't seem to formulate the actual fallacy that show the modified generalization that excludes the false_scotsman leads to a fallacy. Any help in formulating the theorem, not asking for a proof, just something to help me set me on the right course.

Isaac van Bakel (Aug 14 2023 at 13:43):

Interesting problem! Since the fallacy is informal, there's no real "right" way to state such a theorem. Indeed, sometimes excluding a couterexample from a set does rescue a theorem.

I think you want to capture that the condition filtering out the false Scotsman is rhetorical - perhaps by requiring that the "trueness" condition is trivial i.e. `(forall scotsman, In scotsman scotsmen -> IsTrue scotsman) \/ (forall scotsman, In scotsman scotsmen -> ~(IsTrue scotsman))`? Then you'll likely also need that there exist some true Scotsmen...

Julio Di Egidio (Aug 14 2023 at 15:36):

Indeed interesting problem. I take the essence of this fallacy is "the ruling out of all counter-examples", and here is a formalization that I'd think captures that notion and what it practically boils down to...

``````(** No True Scotsman Moves *)

Parameter People : Set.

Parameter scottish : People -> Prop.
Parameter moves : People -> Prop.

(* "Generalized" statement: *)
Definition no_scotsman_moves :=
forall p, scottish p -> ~ moves p.

(* Counter-example: *)
Definition scotsman_q_moves :=
exists q, scottish q /\ moves q.

Lemma this_theory_is_false :
scotsman_q_moves -> ~ no_scotsman_moves.

(* Re-stated to exclude exceptions (!): *)
Definition no_scotsman_moves' :=
forall p, scottish p <-> ~ moves p.

(* Still a contradiction, but first come first served... *)
Lemma this_theory_is_false' :
no_scotsman_moves' -> ~ scotsman_q_moves.
``````

Thomas Dziedzic (Aug 14 2023 at 16:44):

wow, thanks for the hints! I will try to use these hints if not all of Julio's proposed theorem definition to prove it myself.

Thomas Dziedzic (Aug 14 2023 at 16:45):

don't have time atm, but will try this evening and post a solution if I find one/remember to post it :)

Thomas Dziedzic (Aug 14 2023 at 17:52):

had some extra time right now, and it turns out the theorem was harder to state for me than proving Julio's setup :)

``````(** No True Scotsman Moves *)

Parameter People : Set.

Parameter scottish : People -> Prop.
Parameter moves : People -> Prop.

(* "Generalized" statement: *)
Definition no_scotsman_moves :=
forall p, scottish p -> ~ moves p.

(* Counter-example: *)
Definition scotsman_q_moves :=
exists q, scottish q /\ moves q.

Lemma this_theory_is_false :
scotsman_q_moves -> ~ no_scotsman_moves.
Proof.
unfold scotsman_q_moves, no_scotsman_moves.
intros [scotsman [Hscot Hmove]] Hgen.
apply (Hgen scotsman).
- assumption.
- assumption.
Qed.

(* Re-stated to exclude exceptions (!): *)
Definition no_scotsman_moves' :=
forall p, scottish p <-> ~ moves p.

(* Still a contradiction, but first come first served... *)
Lemma this_theory_is_false' :
no_scotsman_moves' -> ~ scotsman_q_moves.
Proof.
unfold no_scotsman_moves', scotsman_q_moves, not.
intros Hiff [scotsman [Hscottish Hmoves]].
destruct (Hiff scotsman) as [Hfal Hgen].
apply Hfal.
- assumption.
- assumption.
Qed.
``````

Julio Di Egidio (Aug 14 2023 at 19:14):

Indeed, especially with these logical puzzles, whether a formalization captures the original problem/notion is the really difficult question...

Karl Palmskog (Aug 14 2023 at 19:21):

if you want to formalize "fallacies" (another one that comes to mind is immovable object meets unstoppable force) I recommend doing it inside a `Section` with only `Variables`/`Hypotheses`, and then proving `False` at the end. That way, the sequence of definitions/theorems can at least be used/validated from outside the section

Last updated: Jun 13 2024 at 19:02 UTC