Skip to content

Commit

Permalink
Note that class variables as postulates are fine
Browse files Browse the repository at this point in the history
Attempt to resolve a comment from Scott Fenton (@sctfn).

Signed-off-by: David A. Wheeler <dwheeler@dwheeler.com>
  • Loading branch information
david-a-wheeler committed Oct 21, 2024
1 parent cd40451 commit 0c028ae
Showing 1 changed file with 6 additions and 3 deletions.
9 changes: 6 additions & 3 deletions set.mm
Original file line number Diff line number Diff line change
Expand Up @@ -431162,9 +431162,12 @@ be applied for new theorems (formerly, the class and wff variables
<p>You should read any statement starting with ` |- `
and having one or more unbound set variable(s) as universally
quantified over those
variables. So when you see ` |- 0 < k ` that's saying " ` 0 < k ` is
derivable in the empty context" which is a strong statement,
equivalent to ` A. k 0 < k ` which without further context is false.
variables. So if you state ` |- 0 < k ` , say as a postulate,
that's saying " ` 0 < k ` is derivable in the empty context"
which is a strong statement,
equivalent to ` A. k 0 < k ` , which without further context is false.
The same is not true for class variables (e.g., ` 0 < K ` is typically
safe to postulate).

<p><b>Additional rules for definitions</b>

Expand Down

0 comments on commit 0c028ae

Please sign in to comment.