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.

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...

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.
```

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.

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

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.
```

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

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