Dari Claim ke Graph of Accepted Facts

Dari Claim ke Graph of Accepted Facts Gambar: dibuat dengan Google Gemini

Realitas adalah sistem terbuka. Catatan datang terlambat. Saksi mencabut kesaksiannya. Sensor dikalibrasi ulang. Kebijakan berubah. Pada titik mana pun kita tidak bisa mengatakan bahwa semua observasi yang relevan telah tiba, karena kita bahkan tidak tahu apa yang masih belum ditemukan.

Tindakan berbeda. Menagih, membayar, memberi akses, membunyikan alarm: masing-masing menuntut jawaban yang tertutup. Sebuah keputusan harus berakhir bahkan ketika realitas tidak. Antara dunia yang terbuka dan tindakan yang terbatas terdapat celah struktural. Keyakinan model yang lebih besar, rantai penalaran yang lebih panjang, atau satu lapisan agen tambahan tidak dapat menutup celah itu.

Pertanyaan pertama karena itu bukan, “Apa yang benar?” Melainkan:

Dalam dunia claim yang tak diketahui ujungnya, siapa yang boleh menetapkan premis untuk keputusan ini, di bawah aturan apa?

Yang masuk ke dalam sistem bukanlah peristiwa itu sendiri. Melainkan kontrak, catatan pembayaran, log sensor, video, kesaksian, atau pesan: fragmen yang dihasilkan oleh seorang pengamat, pada suatu waktu, melalui suatu transformasi, dalam suatu ruang lingkup, dengan mode kegagalan tertentu. Sistem harus menerima ini sebagai Claim, bukan fakta.

Namun menyimpan Claim saja tidak cukup untuk bertindak. Claim dapat saling bertentangan. Catatan yang hilang bisa berarti peristiwa itu tidak pernah terjadi, atau sekadar berarti pengumpulan datanya gagal. Beberapa Claim mungkin harus digabungkan untuk menurunkan satu premis. Jika buku besar Claim yang terbuka langsung dimasukkan ke mesin penilai, pengumpulan, penetapan fakta, dan penerapan aturan akan runtuh kembali menjadi satu tindakan yang buram.

Yang kita butuhkan adalah prosedur eksplisit yang menyusun keadaan faktual yang diizinkan untuk keputusan tertentu. Saya menyebut prosedur itu Projection, dan hasilnya sebuah Graph of Accepted Facts, atau GAF.

Open Claims
    │
    ▼
Projection
    │  evaluation · conflict resolution · derivation · absence policy
    ▼
Graph of Accepted Facts (GAF)
    │
    ▼
Closure
    │  GAF · scope · policy · rules · runtime frozen
    ▼
Deterministic Verdict
    │
    ▼
Authorized Action
    │
    └── new evidence · policy change · appeal · defect
                                  │
                                  ▼
                           Reopen / Re-projection

Intinya bukan mengumpulkan lebih banyak fakta. Melainkan memisahkan penyusunan premis penilaian dari komputasi atas premis tersebut.

Input yang terbatas belum tentu dunia yang tertutup

Sekumpulan Claim yang terbatas tidak membuat dunia menjadi tertutup. Jika pembayaran tidak muncul di suatu basis data, kita tidak bisa langsung menyimpulkan bahwa tidak ada pembayaran yang terjadi. Catatan itu bisa saja hilang, tertunda, salah arah, atau ditahan oleh institusi lain.

Projection karena itu harus menetapkan makna dari ketiadaan, bukan sekadar daftar input:

Sumber mana yang dianggap lengkap untuk subjek, predikat, rentang, dan periode ini?
Di mana asumsi dunia tertutup boleh diterapkan?
Apakah catatan yang hilang berarti false atau unknown?
Bagaimana negasi eksplisit dibedakan dari data yang hilang?
Apa yang harus dikembalikan sistem ketika bukti tidak cukup?

Makalah dasar Raymond Reiter On Closed World Data Bases memformalkan langkah krusial ini: di bawah asumsi dunia tertutup, kegagalan membuktikan literal dasar positif dapat memberi lisensi untuk negasinya. Langkah itu berguna justru karena tidak selalu aman secara universal. Ia membutuhkan batas yang dinyatakan secara eksplisit.

Misalkan sebuah bank menyediakan buku besar transaksi final untuk satu rekening dan satu periode, dan kebijakan Projection menerima buku besar itu sebagai lengkap dalam ruang lingkup tersebut. Ketiadaan kemudian dapat dihitung sebagai bukti bahwa tidak ada transaksi yang cocok di sana. Ketiadaan referensi pembayaran dalam arsip pesan seorang penyewa tidak membuktikan apa pun semacam itu. Satu sumber tertutup untuk kueri yang dinyatakan; sumber lain tetap terbuka.

Closure bukanlah pernyataan “kami sudah membaca sejauh ini.” Ia adalah kontrak yang mendefinisikan di mana ketiadaan itu sendiri menjadi informasi yang dapat dihitung.

Projection bukan tombol yang mempromosikan Claim menjadi fakta

Projection tidak dapat direduksi menjadi menempelkan accepted, rejected, atau held pada seluruh Claim. Claim yang nyata jarang sebersih itu.

“Saya mengirim sewa pada tanggal lima” mungkin memiliki tanggal yang terverifikasi tetapi tujuan yang belum terverifikasi.
Dua catatan independen mungkin diperlukan untuk menetapkan satu pembayaran.
Satu Claim dapat mendukung satu Proposition dan membantah Proposition lain.
Sebuah fakta dapat diturunkan meskipun tidak ada sumber yang menyatakannya secara verbatim.
Sumber yang andal masih dapat belum terselesaikan mengenai peristiwa mana yang digambarkan catatannya.

Evaluation bersifat relasional, bukan bendera pada satu Claim utuh. Ia menghubungkan satu atau lebih Claim, sebuah Proposition atomik, dan sebuah Projection tertentu. Derivation kemudian menggabungkan Evaluation, premis yang sebelumnya diterima, dan aturan eksplisit untuk menghasilkan sebuah Accepted Fact.

Claims ───────┐
Proposition ──┼── Evaluation ── accepted / rejected / unknown
Projection ───┘                     │
                                   ▼
                       Derivation ── Claims · Facts · Rules
                                   │
                                   ▼
                            Accepted Fact

Sebuah Claim menyimpan siapa yang menyatakan atau mengamati apa. Proposition adalah pernyataan terkecil yang sedang dievaluasi. Evaluation mencatat bagaimana Claim-Claim tersebut memengaruhi Proposition itu di bawah satu Projection. Derivation adalah objek pembuktian yang menunjukkan bagaimana hasil itu dihasilkan. Accepted Fact adalah premis yang diizinkan prosedur ini untuk digunakan dalam penilaian ini.

Claim yang sama karena itu dapat menghasilkan Accepted Fact yang berbeda—atau tidak sama sekali—di bawah tujuan, batas waktu, beban pembuktian, atau otoritas yang lain. Accepted Fact bukanlah kebenaran mutlak tentang seluruh realitas. Ia adalah premis yang diizinkan untuk digunakan dalam batas keputusan yang dinyatakan.

Mengapa hasilnya adalah sebuah graf

Premis dari sebuah penilaian bukanlah kalimat-kalimat yang terisolasi. Siapa membayar siapa, kapan, berapa banyak, di bawah kontrak yang mana, untuk kewajiban yang mana, dan apakah kontrak itu masih berlaku saat itu adalah pernyataan-pernyataan yang saling terhubung.

Sebuah Graph of Accepted Facts memuat premis-premis itu dan relasi semantiknya, bersama dengan derivation dan provenance yang menghasilkannya:

entitas, tindakan, waktu, kuantitas, dan keadaan;
Claim yang mendukung atau membantah setiap Proposition;
sumber asli dan pelaku yang bertanggung jawab;
Evaluation dan aturan derivasi;
alternatif yang ditolak atau belum terselesaikan;
relasi temporal, logis, dan supersesi.

Tujuan graf ini bukan penjelasan dekoratif. Melainkan dependensi yang dapat ditelusuri mesin.

Berangkat dari sebuah Verdict, seorang auditor harus dapat menelusuri turun melalui GAF dan aturannya sampai ke Claim asli. Berangkat dari Claim atau sumber yang tidak berlaku lagi, sistem harus dapat menemukan setiap Accepted Fact, Closure, Verdict, dan Action yang mungkin memerlukan peninjauan ulang.

Provenance saja tidak cukup. Analisis dampak yang lengkap juga memerlukan dependensi derivasi, dependensi negatif, kondisi agregat, dan ruang lingkup kebijakan. Sebuah kesimpulan mungkin bergantung bukan pada Claim yang ada, tetapi pada ketiadaan yang dinyatakan dari Claim mana pun yang memenuhi syarat. PROV-O: The PROV Ontology menstandardisasi provenance yang interoperabel di sekitar entitas, aktivitas, agen, dan relasi yang terkualifikasi; beban tambahan GAF adalah menjaga status penerimaan yang spesifik terhadap keputusan serta dependensi negatif yang diperlukan untuk membuka kembali penilaian.

Ini adalah model data logis, bukan mandat basis data graf. Basis data relasional, penyimpanan objek yang beralamat konten, log peristiwa append-only, atau basis data graf semuanya dapat mengimplementasikannya. Penyimpanan fisik itu sah jika ia menjaga node, relasi bertipe, silsilah, dan kueri dependensi tanpa kehilangan makna.

Closure lebih besar daripada GAF

GAF menyimpan Accepted Facts serta Derivation dan Provenance-nya. Closure lebih besar daripada GAF: ia membekukan secara persis GAF mana yang digunakan, untuk pertanyaan apa, di bawah kondisi apa. Ia adalah kontrak pemutaran ulang untuk keputusan tersebut.

Sebuah Closure setidaknya harus memuat:

pertanyaan dan tujuan dari penilaian;
peristiwa, subjek, dan ruang lingkup temporal;
snapshot GAF yang persis dan pengenal integritasnya;
deklarasi kelengkapan dan penanganan ketiadaan, negasi, dan hal yang tidak diketahui;
kebijakan Projection dan versi implementasinya;
aturan Verdict dan versi mesinnya;
kondisi runtime seperti presisi numerik, pengurutan, dan pemecah seri;
aturan kanonikalisasi yang diperlukan untuk mengidentifikasi graf yang sama lagi.

Jika Closure yang sama dieksekusi di runtime yang sama menghasilkan Verdict yang berbeda, lapisan komputasinya cacat. Jika Closure-nya berbeda, ketidaksepakatan itu dapat dilokalisasi ke input, kebijakan Projection, Accepted Facts, aturan, atau runtime.

Determinisme bukan berarti mengetahui realitas dengan sempurna. Ia berarti bahwa dunia tertutup yang sama harus dihitung dengan cara yang sama.

Ikuti satu kasus sampai tuntas

Seorang pemilik rumah menyatakan bahwa sewa bulan Juli belum dibayar. Seorang penyewa menyatakan bahwa sewa itu telah ditransfer pada tanggal lima. Buku besar bank yang final menunjukkan bahwa pemilik rumah menerima seribu dolar pada hari itu, tetapi memo transfer itu kosong. Kontrak mensyaratkan seribu dolar paling lambat tanggal lima setiap bulan.

Open Claim Ledger menyimpan keempat catatan tanpa membiarkan yang satu menimpa yang lain.

Claim	Isi	Status sumber
Claim A	sewa bulan Juli belum dibayar	pernyataan pemilik rumah
Claim B	sewa ditransfer pada tanggal lima	pernyataan penyewa
Claim C	rekening pemilik rumah menerima seribu dolar pada tanggal lima	buku besar bank yang final
Claim D	sewa bulanan seribu dolar, jatuh tempo tanggal lima	kontrak yang sah

Projection mempersempit pertanyaan menjadi: “Apakah tunggakan sewa bulan Juli telah ditetapkan?” Ia menerima buku besar bank sebagai lengkap untuk rekening dan periode tersebut. Ia juga menerapkan kebijakan yang tidak menyimpulkan alokasi ke suatu utang tertentu tanpa memo atau kesepakatan terpisah.

Claim C dan Claim D mendukung Proposition yang diterima. Tanggal dan jumlah dari Claim B didukung oleh Claim C, tetapi alokasinya ke sewa bulan Juli tetap tidak diketahui. Claim A adalah pernyataan salah satu pihak tentang kesimpulan yang diinginkannya, bukan bukti independen atas tidak terbayarnya sewa, sehingga ia tidak menjadi Accepted Fact hanya karena diulang.

GAF mencatat:

The contract required monthly payment by the fifth.       [accepted]
The landlord received the contractual amount that day.    [accepted]
Allocation of that payment to the July debt is unresolved.[unknown]
July rent delinquency has not been established.            [not derived]

Closure mengikat GAF ini dengan kebijakan Projection, ruang lingkup kelengkapan buku besar, batas waktu, dan mesin Verdict. Verdict-nya bukan delinquent; melainkan undetermined. Authorized Action karena itu bukan surat penagihan, melainkan permintaan untuk menetapkan alokasi.

Belakangan, sebuah bukti transfer asli yang bertuliskan memo “sewa Juli” tiba sebagai Claim baru. Closure yang lama tetap disimpan. Sebuah peristiwa Reopen memulai Projection baru. Jika memo itu diterima, GAF baru menerima alokasinya, dan Closure baru menghasilkan paid sebagai Verdict.

Projection dalam contoh ini bukanlah pemungutan suara tentang siapa yang terdengar lebih kredibel. Ia menetapkan pertanyaan, batas kelengkapan, Proposition atomik, makna dari data yang hilang, dan aturan derivasi yang diperlukan untuk menyusun keadaan faktual yang dapat diputuskan.

Simpan keputusan sebagai kontrak

Contoh ini masih memiliki kemacetan. Jika setiap pembayaran tanpa memo mengharuskan pemilik rumah mengonfirmasi alokasi, ketidakpastian itu belum dihilangkan; ia hanya dipindahkan ke antrean persetujuan manusia.

Konfirmasi pertama seharusnya menyelesaikan kasus itu. Pola yang berulang seharusnya melakukan lebih: menyimpan keputusan sebagai kontrak yang dapat menjadi input Projection di masa depan.

Misalkan pemilik rumah mengonfirmasi pembayaran itu dan kedua pihak menyetujui aturan ini:

Sebuah pembayaran dialokasikan ke sewa bulan berjalan ketika ia tiba dari rekening terdaftar penyewa sebelum jatuh tempo, sama dengan jumlah kontraktual, dan tidak ada utang lain yang belum lunas. Kasus yang melanggar syarat apa pun memerlukan peninjauan.

Itu menghasilkan empat catatan yang berbeda:

Case Decision    ── this payment satisfied the July rent
Policy Candidate ── matching future payments may satisfy monthly rent
Ratified Contract── authorized conditions, exceptions, effective date, version
Policy Exception ── ambiguity outside the contract returns to human review

Closure berikutnya merujuk pada versi kebijakan yang telah diratifikasi itu. Claim yang cocok kemudian dapat diproyeksikan tanpa menanyakan pertanyaan yang sama lagi kepada pemilik rumah; hanya pengecualian baru yang mengonsumsi penilaian manusia. Keputusan manusia itu digunakan sekali, sementara struktur yang telah diberi wewenang terus bekerja.

Namun satu keputusan belum menjadi kebijakan. Sistem tidak boleh diam-diam mengubah satu konfirmasi menjadi preseden. Orang yang berwenang harus meratifikasi ruang lingkup aturan itu, pengecualiannya, tanggal berlakunya, dan apakah ia berlaku surut. Sampai saat itu, catatan kasus tersebut hanyalah sebuah Policy Candidate. Jika kontrak baru tidak secara eksplisit berlaku surut, ia mengatur Closure yang akan datang dan tidak menulis ulang Closure sebelumnya.

Ini menambahkan lingkar penyimpanan kedua pada GAF. Claim menyimpan apa yang masuk dari dunia. GAF dan Closure menyimpan apa yang diterima oleh sebuah penilaian tertentu. Kebijakan yang telah diratifikasi menyimpan bagaimana seorang manusia yang berwenang menyelesaikan ambiguitas yang berulang, sehingga Projection berikutnya dimulai dengan kontrak yang lebih kuat alih-alih kemacetan yang sama.

Kesalahan yang berbeda memerlukan perbaikan yang berbeda

Begitu Projection, Verdict, dan Action dipisahkan, satu “hasil yang salah” terurai menjadi kegagalan-kegagalan yang berbeda:

melewatkan Claim yang relevan adalah kesalahan pengumpulan;
mengevaluasi sumber atau Proposition secara keliru adalah kesalahan Projection;
menerapkan aturan yang salah pada Accepted Facts yang benar adalah kesalahan komputasi;
menyajikan Verdict yang benar secara tidak akurat adalah kesalahan komunikasi;
mengeksekusi Verdict yang benar terhadap target, batas, atau otoritas yang salah adalah kesalahan Action.

Taksonomi ini tidak menghapuskan kesalahan. Ia memberi tahu kita apa yang harus dibuka kembali.

Kesalahan pengumpulan memerlukan Claim lain. Kesalahan Projection memerlukan peninjauan ulang atas Evaluation dan Derivation. Kesalahan komputasi dapat menjaga Closure tetap utuh sambil memperbaiki dan membandingkan mesinnya. Kesalahan Action tidak boleh menulis ulang fakta; ia memerlukan pembatalan, koreksi, atau kompensasi di dunia luar.

Menyebut semua ini “modelnya salah” menghancurkan perbedaan itu. Begitu penyebabnya hilang, sistem tidak dapat membuktikan apa yang berubah setelah perbaikan.

Accepted Fact bukan otoritas untuk bertindak

Accepted Fact tidak memberikan kekuasaan. “Sewa itu tertunggak” dan “sistem ini boleh mengirim surat penagihan” adalah Proposition yang berbeda.

Mesin Verdict mengonsumsi sebuah Closure dan menghasilkan penilaian beserta jejak komputasinya. Authorized Action harus secara terpisah memeriksa:

siapa yang mengizinkan efek tersebut;
subjek dan objek mana yang menjadi sasarannya;
jumlah dan batas frekuensi yang berlaku;
apakah pengulangan bersifat idempoten;
tanda terima apa yang membuktikan eksekusi;
bagaimana efek yang keliru dapat dibatalkan atau dikompensasi.

Produksi fakta, penilaian, dan eksekusi terpisah karena masing-masing menjalankan jenis otoritas yang berbeda.

Dunia yang tertutup harus tetap dapat dibuka kembali

Sebuah Closure harus tidak dapat diubah tanpa berpura-pura menjadi kebenaran abadi. Bukti mungkin tiba terlambat. Sebuah sumber mungkin terbukti palsu. Cacat kebijakan mungkin ditemukan. Pihak yang terdampak mungkin mengajukan banding.

Menimpa hasil lama akan menghancurkan penjelasan atas tindakan yang diambil pada saat itu. Reopen karena itu adalah peristiwa baru, bukan penyuntingan atas Closure lama.

Bukti baru, perubahan kebijakan, banding, atau laporan cacat dicatat. Graf dependensi mengidentifikasi Closure yang mungkin terdampak. Jika prosedur yang berwenang mengizinkan pembukaan kembali, Projection baru menghasilkan GAF, Closure, dan Verdict baru. Hasil baru menyatakan apa yang digantikannya tanpa menimpa sejarah.

Jika sebuah Action telah mengubah dunia, penghitungan ulang tidak dapat membalikkannya. Pembatalan, pemberitahuan koreksi, pengembalian dana, dan kompensasi adalah Action baru dengan otorisasi dan tanda terimanya sendiri.

Kemampuan dibuka kembali tidak melemahkan closure. Closure justru menjadi sah ketika sistem menjaga apa yang telah ditetapkan dan hanya mengizinkan penggantian melalui prosedur yang dinyatakan.

LLM tidak dapat menggantikan batas itu

Sebagian besar aplikasi LLM end-to-end mencampur interpretasi pertanyaan, pengambilan data, pemilihan sumber, penetapan fakta, penerapan aturan, dan ekspresi dalam satu generasi. Jika Claim yang diterima dan ditolak tidak dieksternalisasi, jawaban yang sama tidak membuktikan dasar yang sama. Jawaban yang berubah tidak mengungkapkan apakah batas input atau komputasinya yang berubah.

Penjelasan panjang atau jejak penalaran yang dihasilkan tidak menyelesaikan masalah ini. Penjelasan pasca-hoc bukanlah catatan eksekusi dari input, aturan, dan otoritas yang sebenarnya digunakan.

LLM tetap berguna di sekitar batas itu. Ia dapat mengekstrak kandidat Claim dari sumber yang tidak terstruktur, mengusulkan Proposition atomik, menjelaskan konflik dan hal yang tidak diketahui, menyusun draf kebijakan Projection, dan menerjemahkan Verdict yang telah ditetapkan ke dalam bahasa manusia.

Namun usulan bukanlah penerimaan. Claim, pemetaan, Evaluation, atau aturan yang dihasilkan LLM harus menjadi input yang berversi dengan provenance dan melewati prosedur yang berwenang. Otoritas final untuk tindakan berkonsekuensi tinggi tidak boleh tetap tersembunyi di dalam generasi bahasa alami.

Kontribusinya adalah rantainya

Komponen-komponennya tidak semuanya baru. Penalaran dunia tertutup, provenance, truth-maintenance system, event sourcing, mesin aturan, penetapan fakta hukum, dan banding memiliki sejarah panjang. On Closed World Data Bases menetapkan perbedaan dunia terbuka/tertutup, sementara PROV-O: The PROV Ontology menstandardisasi model graf untuk menelusuri entitas melalui aktivitas dan agen yang bertanggung jawab.

Kontribusinya adalah rantainya, disusun sebagai satu protokol tanggung jawab:

Claims → Projection → GAF → Closure → Verdict → Action → Reopen

Setiap panah adalah batas otoritas dan kesalahan, bukan sekadar transformasi data. Pelaku yang menyimpan Claim, otoritas yang menerima premis, mesin yang menghitung Verdict, dan gerbang yang mengubah dunia beroperasi di bawah kontrak yang berbeda. Catatan-catatan mereka saling terhubung, tetapi tidak ada tahap yang diam-diam mewarisi otoritas dari tahap yang lain.

GAF bukanlah penemuan basis data lain. Ia adalah usulan untuk membuat seluruh perjalanan dari claim yang terbuka menuju fakta yang dapat ditindaklanjuti dapat diaudit, direproduksi, dan dibanding.

Tujuannya adalah closure yang terkendali, bukan kebenaran yang sempurna

Kita tidak dapat membangun sistem yang mengetahui seluruh dunia yang terbuka. Kita dapat membangun sistem yang menyatakan informasi mana yang diterimanya sebagai premis, dan mengapa.

Open Claims menyimpan ketidaksepakatan dan ketidakpastian. Projection menetapkan tujuan, ruang lingkup, beban pembuktian, dan makna dari ketiadaan. GAF menghubungkan premis yang diterima dengan relasi dan silsilahnya. Closure membekukan kondisi untuk pemutaran ulang. Verdict menghitung atas input yang tertutup. Action mengubah realitas di bawah otoritas yang terpisah. Reopen meninjau ulang batas itu tanpa menghapus sejarah.

Dengan siklus ini, kesalahan tidak lagi tetap menjadi satu halusinasi yang buram. Kita dapat membedakan apa yang terlewat oleh sistem, apa yang diterimanya secara keliru, apa yang salah dihitungnya dari premis yang diterima, dan apa yang salah dieksekusinya setelah penilaian yang benar.

Memproyeksikan Claim ke dalam GAF bukanlah cara untuk membuat mesin tak terkalahkan. Ia menetapkan apa yang menjadi dasar penilaian mesin sehingga penilaian itu dapat direproduksi, ditantang, dan dikoreksi.

Aforisme “matematika benar karena ia menghitung di dalam sistem tertutup” menunjuk pada fakta yang lebih sempit dan dapat dipertahankan. Begitu aksioma, definisi, dan aturan inferensi ditetapkan, sebuah derivasi di dalam batas formal itu dapat diperiksa dan diputar ulang (Formalism in the Philosophy of Mathematics). Ini tidak membuat setiap kebenaran matematis dapat dihitung, setiap proposisi dapat diputuskan, atau setiap sistem aksiomatik lengkap. Closure menjamin reproduktibilitas dari sebuah derivasi yang diterima, bukan kemahatahuan.

Penilaian dunia nyata membutuhkan disiplin yang sama sebelum komputasi. GAF bukanlah kebenaran itu sendiri. Ia adalah dunia tertutup yang menetapkan premis mana yang diterima dari realitas yang terbuka, sehingga sebuah verdict dapat direproduksi—dan dipersengketakan—di dalamnya.

Bacaan lanjutan (eksternal)

On Closed World Data Bases — penjelasan asli Raymond Reiter tentang evaluasi kueri dunia terbuka dan tertutup
PROV-O: The PROV Ontology — rekomendasi W3C untuk provenance yang interoperabel
Formalism in the Philosophy of Mathematics — penjelasan formalis tentang kebenaran matematis dalam sistem yang diatur aturan