---
record_id: HP-HTFOL-DEJING-LEX
classification: De Jing FOL Profile Lexicon
work: De Jing
status: prototype
scope: Adaptor House governance lexicon for De Jing formalization
inherits: HP-HTFOL-MASTER
---

# De Jing FOL Lexicon

This shared lexicon records predicates and sentence forms used by the De Jing line-commentary pages.

Namespace: use `dejing`, not `dj`, because `dj` collides with both De Jing and Dao Jing.

## De Jing 1.1 Prototype

Source sentence: 上德不德，是以有德；

English witness: Highest virtue does not make a show of virtue; therefore it has virtue.

```text
∀x ((Virtue(x) ∧ Highest(x) ∧ ¬DisplaysVirtue(x)) → HasVirtue(x))
```

## Predicates

| Predicate | Definition |
| --- | --- |
| `Virtue(x)` | `x` is virtue, 德, as a formal term. |
| `Highest(x)` | `x` has the rank marked by 上. |
| `DisplaysVirtue(x)` | `x` exhibits virtue as an overt display. |
| `HasVirtue(x)` | `x` possesses or instantiates virtue. |
| `SentenceClaim(s, p)` | Sentence `s` bears proposition `p`; the translation witnesses that proposition without becoming it. |
| `∀x` | Universal quantification over any candidate object `x` in the claim domain. |
| `→` | Material implication; the formal counterpart to the sentence's consequence structure. |

## Witness And Syntax Layers

| Predicate | Definition |
| --- | --- |
| `EnglishLine(el)` | `el` is an English line-level witness. |
| `EnglishSyntax(ex)` | `ex` is an English syntactic parse. |
| `EnglishSegment(es)` | `es` is an English segment within a line. |
| `ChineseLine(cl)` | `cl` is a Chinese line-level witness. |
| `ChineseSegment(cs)` | `cs` is a Chinese segment within a line. |
| `ChineseSyntaxModern(csm)` | `csm` is a modern Chinese syntactic parse. |
| `ChineseSyntaxArchaic(csa)` | `csa` is an archaic Chinese syntactic parse. |

## Witness Relations

| Relation | Definition |
| --- | --- |
| `Expresses(c, s)` | Chinese segment or line `c` expresses sentence or semantic unit `s`. |
| `Renders(e, s)` | English segment or line `e` renders sentence or semantic unit `s`. |
| `ProvisionalAlignment(e, c)` | English witness `e` is provisionally aligned with Chinese witness `c`. |

## Proof Form For De Jing 1.1

```text
1. Assume arbitrary x.
2. Assume Virtue(x) ∧ Highest(x) ∧ ¬DisplaysVirtue(x).
3. From line 2, retain all three conjuncts.
4. Interpretive premise from De Jing 1.1:
   (Virtue(x) ∧ Highest(x) ∧ ¬DisplaysVirtue(x)) → HasVirtue(x).
5. Therefore HasVirtue(x).
6. Discharge assumption 2: (Virtue(x) ∧ Highest(x) ∧ ¬DisplaysVirtue(x)) → HasVirtue(x).
7. Universal generalization over arbitrary x:
   ∀x ((Virtue(x) ∧ Highest(x) ∧ ¬DisplaysVirtue(x)) → HasVirtue(x))
8. ⊢ ∀x ((Virtue(x) ∧ Highest(x) ∧ ¬DisplaysVirtue(x)) → HasVirtue(x))
9. ∴ SentenceClaim(sentence_de_01_001, ∀x ((Virtue(x) ∧ Highest(x) ∧ ¬DisplaysVirtue(x)) → HasVirtue(x)))
```