Stream: Coq users

Topic: No True Scotsman fallacy formalization.


view this post on Zulip 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.

view this post on Zulip 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...

view this post on Zulip 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.

(* Contradiction... *)
Lemma this_theory_is_false :
  scotsman_q_moves -> ~ no_scotsman_moves.
Proof. (* Your proof here. *) Admitted.

(* 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. (* Your proof here. *) Admitted.

view this post on Zulip 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.

view this post on Zulip 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 :)

view this post on Zulip 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.

(* Contradiction... *)
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.

view this post on Zulip 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...

view this post on Zulip 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